A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by BORSUK_1:def 5;
A2: dom (pr1 f) = dom f by MCART_1:def 12;
A3: dom f = the carrier of Y by FUNCT_2:def 1;
rng (pr1 f) c= the carrier of S

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pr1 f) or y in the carrier of S )
assume y in rng (pr1 f) ; :: thesis: y in the carrier of S
then consider x being set such that
A4: x in dom (pr1 f) and
A5: (pr1 f) . x = y by FUNCT_1:def 5;
A6: (pr1 f) . x = (f . x) `1 by A2, A4, MCART_1:def 12;
f . x in rng f by A2, A4, FUNCT_1:def 5;
hence y in the carrier of S by A1, A5, A6, MCART_1:10; :: thesis: verum

end;

hence pr1 f is Function of Y,S by A2, A3, FUNCT_2:4; :: thesis: verum