A7: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by BORSUK_1:def 5;
A8: dom (pr2 f) = dom f by MCART_1:def 13;
A9: dom f = the carrier of Y by FUNCT_2:def 1;
rng (pr2 f) c= the carrier of T

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pr2 f) or y in the carrier of T )
assume y in rng (pr2 f) ; :: thesis: y in the carrier of T
then consider x being set such that
A10: x in dom (pr2 f) and
A11: (pr2 f) . x = y by FUNCT_1:def 5;
A12: (pr2 f) . x = (f . x) `2 by A8, A10, MCART_1:def 13;
f . x in rng f by A8, A10, FUNCT_1:def 5;
hence y in the carrier of T by A7, A11, A12, MCART_1:10; :: thesis: verum

end;

hence pr2 f is Function of Y,T by A8, A9, FUNCT_2:4; :: thesis: verum