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; verum