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 V7() & rng f = [#] Z ) by A1, TOPS_2:def 5;

A4: dom f = [#] Y by A1, TOPS_2:def 5;

( 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

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 V7() & 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

then A3:
(oContMaps (X,f)) * (oContMaps (X,g)) = id (oContMaps (X,Z))
by FUNCT_2:63;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;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

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

then A5:
(oContMaps (X,g)) * (oContMaps (X,f)) = id (oContMaps (X,Y))
by FUNCT_2:63;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;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

( 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