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 5;
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 5 ;
hence [:f,g:] is Function of [:S1,T1:],[:S2,T2:] by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum