let X, Y, Z be non empty TopSpace; :: thesis: ( Y,Z are_homeomorphic implies oContMaps X,Y, oContMaps X,Z are_isomorphic )
given f being Function of Y,Z such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: oContMaps X,Y, oContMaps X,Z are_isomorphic
reconsider f = f as continuous Function of Y,Z by A1, TOPS_2:def 5;
take oContMaps X,f ; :: according to WAYBEL_1:def 8 :: thesis: oContMaps X,f is isomorphic
thus oContMaps X,f is isomorphic by A1, Th21; :: thesis: verum