let S, T be non empty TopStruct ; :: thesis: for f being Function of S,T holds
( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & 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 S,T; :: thesis: ( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f " P is closed ) ) ) )

hereby :: thesis: ( dom f = [#] S & rng f = [#] T & 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 = [#] S & rng f = [#] T & 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 = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def 5; :: 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 ) )

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

assume A3: P is closed ; :: thesis: f " P is closed
f is continuous by A1, TOPS_2:def 5;
hence f " P is closed by A3, PRE_TOPC:def 12; :: thesis: verum

end;

assume f " P is closed ; :: thesis: P is closed
then f .: (f " P) is closed by A1, TOPS_2:72;
hence P is closed by A2, FUNCT_1:147; :: thesis: verum

end;

assume that
A4: dom f = [#] S and
A5: rng f = [#] T and
A6: f is one-to-one and
A7: for P being Subset of T holds
( P is closed iff f " P is closed ) ; :: thesis: f is being_homeomorphism
thus ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A4, A5, A6; :: according to TOPS_2:def 5 :: thesis: ( f is continuous & f /" is continuous )
thus f is continuous :: thesis: f /" is continuous

proof

let P be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( not P is closed or f " P is closed )
thus ( not P is closed or f " P is closed ) by A7; :: thesis: verum

end;

let R be Subset of S; :: according to PRE_TOPC:def 12 :: thesis: ( not R is closed or (f /" ) " R is closed )
assume A8: R is closed ; :: thesis: (f /" ) " R is closed
for x1, x2 being Element of S st x1 in R & f . x1 = f . x2 holds
x2 in R by A4, A6, FUNCT_1:def 8;
then A9: f " (f .: R) = R by T_0TOPSP:2;
(f /" ) " R = f .: R by A5, A6, TOPS_2:67;
hence (f /" ) " R is closed by A7, A8, A9; :: thesis: verum