let T be TopStruct ; :: thesis: for S being non empty TopStruct
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )
let S be non empty TopStruct ; :: thesis: for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )
let f be Function of T,S; :: thesis: ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )

hereby :: thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) implies f is being_homeomorphism )

assume A1: f is being_homeomorphism ; :: thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) ) ) )
then A2: f is continuous by Def5;
thus A3: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A1, Def5; :: thesis: for P being Subset of T holds
( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) )
A4: f " is continuous by A1, Def5;
let P be Subset of T; :: thesis: ( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) )

hereby :: thesis: ( f .: P is closed implies P is closed )

assume A5: P is closed ; :: thesis: f .: P is closed
(f " ) " P = (f " ) " P by A3, Def4
.= f .: P by A3, FUNCT_1:154 ;
hence f .: P is closed by A4, A5, PRE_TOPC:def 12; :: thesis: verum

end;

assume f .: P is closed ; :: thesis: P is closed
then A6: f " (f .: P) is closed by A2, PRE_TOPC:def 12;
A7: f " (f .: P) c= P by A3, FUNCT_1:152;
dom f = [#] T by FUNCT_2:def 1;
then P c= f " (f .: P) by FUNCT_1:146;
hence P is closed by A6, A7, XBOOLE_0:def 10; :: thesis: verum

end;

assume A8: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) ; :: thesis: ( ex P being Subset of T st
( ( P is closed implies f .: P is closed ) implies ( f .: P is closed & not P is closed ) ) or f is being_homeomorphism )
assume A9: for P being Subset of T holds
( P is closed iff f .: P is closed ) ; :: thesis: f is being_homeomorphism
A10: f is continuous

proof

let B be Subset of S; :: according to PRE_TOPC:def 12 :: thesis: ( not B is closed or f " B is closed )
assume A11: B is closed ; :: thesis: f " B is closed
set D = f " B;
B = f .: (f " B) by A8, FUNCT_1:147;
hence f " B is closed by A9, A11; :: thesis: verum

end;

f " is continuous

proof

let B be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( not B is closed or (f " ) " B is closed )
assume A12: B is closed ; :: thesis: (f " ) " B is closed
(f " ) " B = (f " ) " B by A8, Def4
.= f .: B by A8, FUNCT_1:154 ;
hence (f " ) " B is closed by A9, A12; :: thesis: verum

end;

hence f is being_homeomorphism by A8, A10, Def5; :: thesis: verum