A1: dom (pr1 f) = dom f by MCART_1:def 12;
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def 2;
A3: rng (pr1 f) c= the carrier of S
proof
let y be object ; :: 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 object such that
A4: x in dom (pr1 f) and
A5: (pr1 f) . x = y by FUNCT_1:def 3;
( (pr1 f) . x = (f . x) `1 & f . x in rng f ) by A1, A4, FUNCT_1:def 3, MCART_1:def 12;
hence y in the carrier of S by A2, A5, MCART_1:10; :: thesis: verum
end;
dom f = the carrier of Y by FUNCT_2:def 1;
hence pr1 f is Function of Y,S by A1, A3, FUNCT_2:2; :: thesis: verum