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 ) ) ) )
hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) ; :: thesis: for P being Subset of T holds
( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) )
let P be Subset of T; :: thesis: ( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) )
A3: f " is continuous by A1;

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

assume A4: P is closed ; :: thesis: f .: P is closed
f is onto by A2, FUNCT_2:def 3;
then (f ") " P = (f ") " P by A2, Def4
.= f .: P by A2, FUNCT_1:84 ;
hence f .: P is closed by A3, A4; :: thesis: verum

end;

assume A5: f .: P is closed ; :: thesis: P is closed
f is continuous by A1;
then A6: f " (f .: P) is closed by A5;
dom f = [#] T by FUNCT_2:def 1;
then A7: P c= f " (f .: P) by FUNCT_1:76;
f " (f .: P) c= P by A2, FUNCT_1:82;
hence P is closed by A6, A7, XBOOLE_0:def 10; :: thesis: verum

end;

assume that
A8: dom f = [#] T and
A9: rng f = [#] S and
A10: 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 A11: for P being Subset of T holds
( P is closed iff f .: P is closed ) ; :: thesis: f is being_homeomorphism
A12: f is continuous

proof

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

end;

f " is continuous

proof

let B be Subset of T; :: according to PRE_TOPC:def 6 :: thesis: ( not B is closed or (f ") " B is closed )
assume A14: B is closed ; :: thesis: (f ") " B is closed
f is onto by A9, FUNCT_2:def 3;
then (f ") " B = (f ") " B by A10, Def4
.= f .: B by A10, FUNCT_1:84 ;
hence (f ") " B is closed by A11, A14; :: thesis: verum

end;

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