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:]
A1:
pr1 the carrier of S,the carrier of T is continuous Function of [:S,T:],S
by Th39;
pr2 the carrier of S,the carrier of T is continuous Function of [:S,T:],T
by 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 A1, Th41; :: thesis: verum