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: [#] T <> {} ;
A2: [#] S <> {} ;

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 A3: 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 ) ) ) )
hence A4: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) ; :: 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 ) )
A5: ( f " (f .: P) c= P & P c= f " (f .: P) ) by A4, FUNCT_1:76, FUNCT_1:82;
A6: f /" is continuous by A3;

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

assume A7: P is open ; :: thesis: f .: P is open
f is onto by A4;
then (f /") " P = (f ") " P by A4, TOPS_2:def 4
.= f .: P by A4, FUNCT_1:84 ;
hence f .: P is open by A2, A6, A7, TOPS_2:43; :: thesis: verum

end;

assume A8: f .: P is open ; :: thesis: P is open
f is continuous by A3;
then f " (f .: P) is open by A1, A8, TOPS_2:43;
hence P is open by A5, XBOOLE_0:def 10; :: thesis: verum

end;

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

now :: thesis: for B being Subset of T st B is open holds
f " B is open

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

end;

then A14: f is continuous by A1, TOPS_2:43;

now :: thesis: for B being Subset of S st B is open holds
(f /") " B is open

let B be Subset of S; :: thesis: ( B is open implies (f /") " B is open )
assume A15: B is open ; :: thesis: (f /") " B is open
f is onto by A10;
then (f /") " B = (f ") " B by A11, TOPS_2:def 4
.= f .: B by A11, FUNCT_1:84 ;
hence (f /") " B is open by A12, A15; :: thesis: verum

end;

then f /" is continuous by A2, TOPS_2:43;
hence f is being_homeomorphism by A9, A10, A11, A14; :: thesis: verum