A7: dom (pr2 f) = dom f by MCART_1:def 13;
A8: rng (pr2 f) c= C
proof
let x be object ; :: 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 object such that
A9: ( y in dom (pr2 f) & x = (pr2 f) . y ) by FUNCT_1:def 3;
( x = (f . y) `2 & f . y in [:B,C:] ) by A7, A9, Th5, MCART_1:def 13;
hence x in C by MCART_1:10; :: thesis: verum
end;
dom (pr2 f) = A by A7, Def1;
hence pr2 f is Function of A,C by A8, Th2; :: thesis: verum