let S, T be TopSpace; :: thesis: for h being Function of S,T
for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds
g is isomorphic
let h be Function of S,T; :: thesis: for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds
g is isomorphic
let g be Function of (Omega S),(Omega T); :: thesis: ( h = g & h is being_homeomorphism implies g is isomorphic )
assume that
A1: h = g and
A2: h is being_homeomorphism ; :: thesis: g is isomorphic
A3: ( the carrier of S = the carrier of (Omega S) & the carrier of T = the carrier of (Omega T) ) by Lm1;
A4: dom h = [#] S by A2, TOPS_2:def 5;
A5: ( h is one-to-one & rng h = [#] T ) by A2, TOPS_2:def 5;

per cases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;

suppose A6: ( not S is empty & not T is empty ) ; :: thesis: g is isomorphic

then reconsider s = S, t = T as non empty TopSpace ;
reconsider f = g as Function of (Omega s),(Omega t) ;
for x, y being Element of (Omega s) holds
( x <= y iff f . x <= f . y )

proof

let x, y be Element of (Omega s); :: thesis: ( x <= y iff f . x <= f . y )
A7: dom h = the carrier of (Omega s) by A4, Lm1;

hereby :: thesis: ( f . x <= f . y implies x <= y )

assume x <= y ; :: thesis: f . x <= f . y
then consider Y being Subset of s such that
A8: Y = {y} and
A9: x in Cl Y by Def2;
reconsider Z = {(f . y)} as Subset of t by Lm1;
f . x in f .: (Cl Y) by A9, FUNCT_2:43;
then A10: h . x in Cl (h .: Y) by A1, A2, TOPS_2:74;
Im h,y = Z by A1, A7, FUNCT_1:117;
hence f . x <= f . y by A1, A8, A10, Def2; :: thesis: verum

end;

assume f . x <= f . y ; :: thesis: x <= y
then consider Y being Subset of t such that
A11: Y = {(f . y)} and
A12: f . x in Cl Y by Def2;
reconsider Z = {((f " ) . (f . y))} as Subset of s by Lm1;
A13: h " is being_homeomorphism by A2, A6, TOPS_2:70;
A14: f " = f " by A1, A5, Lm1, TOPS_2:def 4
.= h " by A1, A5, TOPS_2:def 4 ;
(f " ) . (f . x) in (f " ) .: (Cl Y) by A12, FUNCT_2:43;
then A15: (h " ) . (h . x) in Cl ((h " ) .: Y) by A1, A13, A14, TOPS_2:74;
A16: x = (f " ) . (f . x) by A1, A5, A7, FUNCT_1:56
.= (f " ) . (f . x) by A1, A5, Lm1, TOPS_2:def 4 ;
A17: y = (h " ) . (h . y) by A5, A7, FUNCT_1:56
.= (f " ) . (f . y) by A1, A5, Lm1, TOPS_2:def 4 ;
A18: dom f = [#] S by A1, A2, TOPS_2:def 5
.= the carrier of S ;
(f " ) .: Y = (f " ) .: Y by A1, A5, Lm1, TOPS_2:def 4
.= f " Y by A1, A5, FUNCT_1:155
.= Z by A1, A3, A5, A11, A17, A18, FINSEQ_5:4 ;
hence x <= y by A1, A14, A15, A16, A17, Def2; :: thesis: verum

end;

hence g is isomorphic by A1, A3, A5, WAYBEL_0:66; :: thesis: verum

end;

suppose ( S is empty or T is empty ) ; :: thesis: g is isomorphic

then reconsider s = S, t = T as empty TopSpace by A4, A5;
( Omega s is empty & Omega t is empty ) ;
hence g is isomorphic by WAYBEL_0:def 38; :: thesis: verum

end;

end;