( dom f = the carrier of Y & dom g = the carrier of Y ) by FUNCT_2:def 1;
then A1: dom <:f,g:> = the carrier of Y by FUNCT_3:50;
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def 2;
hence <:f,g:> is Function of Y,[:S,T:] by A1; :: thesis: verum