set h = [:f,g:];
rng [:f,g:] c= [: the carrier of S2, the carrier of T2:] ;
then A1: rng [:f,g:] c= the carrier of [:S2,T2:] by BORSUK_1:def 2;
dom [:f,g:] = [: the carrier of S1, the carrier of T1:] by FUNCT_2:def 1
.= the carrier of [:S1,T1:] by BORSUK_1:def 2 ;
hence [:f,g:] is Function of [:S1,T1:],[:S2,T2:] by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum