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