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 S holds
( P is open iff f .: P is open ) ) ) )
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 S holds
( P is open iff f .: P is open ) ) ) )
A1: ( [#] S <> {} & [#] T <> {} ) ;

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

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

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

assume A6: P is open ; :: thesis: f .: P is open
(f /" ) " P = (f " ) " P by A5, TOPS_2:def 4
.= f .: P by A5, FUNCT_1:154 ;
hence f .: P is open by A1, A4, A6, TOPS_2:55; :: thesis: verum

end;

assume f .: P is open ; :: thesis: P is open
then A7: f " (f .: P) is open by A1, A3, TOPS_2:55;
A8: f " (f .: P) c= P by A5, FUNCT_1:152;
P c= f " (f .: P) by A5, FUNCT_1:146;
hence P is open by A7, A8, XBOOLE_0:def 10; :: thesis: verum

end;

assume that
A9: ( dom f = [#] S & rng f = [#] T ) and
A10: f is one-to-one and
A11: for P being Subset of S holds
( P is open iff f .: P is open ) ; :: thesis: f is being_homeomorphism

now

let B be Subset of T; :: thesis: ( B is open implies f " B is open )
assume A12: B is open ; :: thesis: f " B is open
B = f .: (f " B) by A9, FUNCT_1:147;
hence f " B is open by A11, A12; :: thesis: verum

end;

then A13: f is continuous by A1, TOPS_2:55;

now

let B be Subset of S; :: thesis: ( B is open implies (f /" ) " B is open )
assume A14: B is open ; :: thesis: (f /" ) " B is open
(f /" ) " B = (f " ) " B by A9, A10, TOPS_2:def 4
.= f .: B by A10, FUNCT_1:154 ;
hence (f /" ) " B is open by A11, A14; :: thesis: verum

end;

then f /" is continuous by A1, TOPS_2:55;
hence f is being_homeomorphism by A9, A10, A13, TOPS_2:def 5; :: thesis: verum