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

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:21
.= (oContMaps X,f) . (g * h) by Def2
.= f * (g * h) by Def2
.= (f * g) * h by RELAT_1:55
.= (id the carrier of Z) * h by A2, TOPS_2:65
.= a by FUNCT_2:23
.= (id (oContMaps X,Z)) . a by FUNCT_1:35 ; :: thesis: verum

end;

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

now

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:21
.= (oContMaps X,g) . (f * h) by Def2
.= g * (f * h) by Def2
.= (g * f) * h by RELAT_1:55
.= (id the carrier of Y) * h by A2, A4, TOPS_2:65
.= a by FUNCT_2:23
.= (id (oContMaps X,Y)) . a by FUNCT_1:35 ; :: thesis: verum

end;

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