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

proof

let x be set ; :: 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 set such that
A3: y in dom (pr1 f) and
A4: x = (pr1 f) . y by FUNCT_1:def 5;
A5: x = (f . y) `1 by A1, A3, A4, MCART_1:def 12;
f . y in [:B,C:] by A1, A3, Th7;
hence x in B by A5, MCART_1:10; :: thesis: verum

end;

hence pr1 f is Function of A,B by A2, Th4; :: thesis: verum