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, Th20; :: thesis: verum

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, Th20; :: thesis: verum