let S, T be TopSpace; :: thesis: ( S,T are_homeomorphic implies Omega S, Omega T are_isomorphic )
assume S,T are_homeomorphic ; :: thesis: Omega S, Omega T are_isomorphic
then consider h being Function of S,T such that
A1: h is being_homeomorphism ;
A2: the carrier of T = the carrier of (Omega T) by Lm1;
the carrier of S = the carrier of (Omega S) by Lm1;
then reconsider f = h as Function of (Omega S),(Omega T) by A2;
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
thus f is isomorphic by A1, Th18; :: thesis: verum