set f = the continuous Function of S,T;
the continuous Function of S,T in the carrier of (ContMaps (S,T)) by Def3;
hence not ContMaps (S,T) is empty ; :: thesis: verum