let S, T be non empty TopSpace; :: thesis: <:(pr2 the carrier of S,the carrier of T),(pr1 the carrier of S,the carrier of T):> is continuous Function of [:S,T:],[:T,S:]
( pr1 the carrier of S,the carrier of T is continuous Function of [:S,T:],S & pr2 the carrier of S,the carrier of T is continuous Function of [:S,T:],T ) by Th39, Th40;
hence <:(pr2 the carrier of S,the carrier of T),(pr1 the carrier of S,the carrier of T):> is continuous Function of [:S,T:],[:T,S:] by Th41; :: thesis: verum