A6: dom (pr2 f) = dom f by MCART_1:def 13;
A7: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def 2;
A8: rng (pr2 f) c= the carrier of T

proof

let y be object ; :: 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 object such that
A9: x in dom (pr2 f) and
A10: (pr2 f) . x = y by FUNCT_1:def 3;
( (pr2 f) . x = (f . x) `2 & f . x in rng f ) by A6, A9, FUNCT_1:def 3, MCART_1:def 13;
hence y in the carrier of T by A7, A10, MCART_1:10; :: thesis: verum

end;

dom f = the carrier of Y by FUNCT_2:def 1;
hence pr2 f is Function of Y,T by A6, A8, FUNCT_2:2; :: thesis: verum