A9: dom (pr2 f) = dom f by MCART_1:def 13;
then A10: dom (pr2 f) = A by Def1;
rng (pr2 f) c= C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (pr2 f) or x in C )
assume x in rng (pr2 f) ; :: thesis: x in C
then consider y being set such that
A11: y in dom (pr2 f) and
A12: x = (pr2 f) . y by FUNCT_1:def 5;
A13: x = (f . y) `2 by A9, A11, A12, MCART_1:def 13;
f . y in [:B,C:] by A9, A11, Th7;
hence x in C by A13, MCART_1:10; :: thesis: verum

end;

hence pr2 f is Function of A,C by A10, Th4; :: thesis: verum