A1: dom (pr1 f) = dom f by MCART_1:def 12;
A2: rng (pr1 f) c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (pr1 f) or x in B )
assume x in rng (pr1 f) ; :: thesis: x in B
then consider y being object such that
A3: ( y in dom (pr1 f) & x = (pr1 f) . y ) by FUNCT_1:def 3;
( x = (f . y) `1 & f . y in [:B,C:] ) by A1, A3, Th5, MCART_1:def 12;
hence x in B by MCART_1:10; :: thesis: verum

end;

dom (pr1 f) = A by A1, Def1;
hence pr1 f is Function of A,B by A2, Th2; :: thesis: verum