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

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