let X, Y, Z be non empty TopSpace; :: thesis: for f being continuous Function of Y,Z st f is being_homeomorphism holds
oContMaps (X,f) is isomorphic
let f be continuous Function of Y,Z; :: thesis: ( f is being_homeomorphism implies oContMaps (X,f) is isomorphic )
set XY = oContMaps (X,Y);
set XZ = oContMaps (X,Z);
assume A1: f is being_homeomorphism ; :: thesis: oContMaps (X,f) is isomorphic
then reconsider g = f " as continuous Function of Z,Y by TOPS_2:def 5;
set Xf = oContMaps (X,f);
set Xg = oContMaps (X,g);
A2: ( f is one-to-one & rng f = [#] Z ) by A1, TOPS_2:def 5;

now :: thesis: for a being Element of (oContMaps (X,Z)) holds ((oContMaps (X,f)) * (oContMaps (X,g))) . a = (id (oContMaps (X,Z))) . a

let a be Element of (oContMaps (X,Z)); :: thesis: ((oContMaps (X,f)) * (oContMaps (X,g))) . a = (id (oContMaps (X,Z))) . a
reconsider h = a as continuous Function of X,Z by Th2;
thus ((oContMaps (X,f)) * (oContMaps (X,g))) . a = (oContMaps (X,f)) . ((oContMaps (X,g)) . a) by FUNCT_2:15
.= (oContMaps (X,f)) . (g * h) by Def2
.= f * (g * h) by Def2
.= (f * g) * h by RELAT_1:36
.= (id the carrier of Z) * h by A2, TOPS_2:52
.= a by FUNCT_2:17
.= (id (oContMaps (X,Z))) . a ; :: thesis: verum

end;

then A3: (oContMaps (X,f)) * (oContMaps (X,g)) = id (oContMaps (X,Z)) by FUNCT_2:63;
A4: dom f = [#] Y by A1, TOPS_2:def 5;

now :: thesis: for a being Element of (oContMaps (X,Y)) holds ((oContMaps (X,g)) * (oContMaps (X,f))) . a = (id (oContMaps (X,Y))) . a

let a be Element of (oContMaps (X,Y)); :: thesis: ((oContMaps (X,g)) * (oContMaps (X,f))) . a = (id (oContMaps (X,Y))) . a
reconsider h = a as continuous Function of X,Y by Th2;
thus ((oContMaps (X,g)) * (oContMaps (X,f))) . a = (oContMaps (X,g)) . ((oContMaps (X,f)) . a) by FUNCT_2:15
.= (oContMaps (X,g)) . (f * h) by Def2
.= g * (f * h) by Def2
.= (g * f) * h by RELAT_1:36
.= (id the carrier of Y) * h by A2, A4, TOPS_2:52
.= a by FUNCT_2:17
.= (id (oContMaps (X,Y))) . a ; :: thesis: verum

end;

then A5: (oContMaps (X,g)) * (oContMaps (X,f)) = id (oContMaps (X,Y)) by FUNCT_2:63;
( oContMaps (X,f) is monotone & oContMaps (X,g) is monotone ) by Th8;
hence oContMaps (X,f) is isomorphic by A5, A3, YELLOW16:15; :: thesis: verum