let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic iff ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S ) )

hereby :: thesis: ( ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S ) implies S,T are_homeomorphic )

assume S,T are_homeomorphic ; :: thesis: ex f being continuous Function of S,T ex g being continuous Function of T,S st
( f * g = id T & g * f = id S )
then consider f being Function of S,T such that
A1: f is being_homeomorphism ;
reconsider f = f as continuous Function of S,T by A1, TOPS_2:def 5;
A2: rng f = [#] T by A1, TOPS_2:def 5;
reconsider g = f " as continuous Function of T,S by A1, TOPS_2:def 5;
take f = f; :: thesis: ex g being continuous Function of T,S st
( f * g = id T & g * f = id S )
take g = g; :: thesis: ( f * g = id T & g * f = id S )
A3: dom f = [#] S by A1, TOPS_2:def 5;
f is one-to-one by A1, TOPS_2:def 5;
hence ( f * g = id T & g * f = id S ) by A2, A3, TOPS_2:52; :: thesis: verum

end;

given f being continuous Function of S,T, g being continuous Function of T,S such that A4: f * g = id T and
A5: g * f = id S ; :: thesis: S,T are_homeomorphic
A6: f is onto by A4, FUNCT_2:23;
then A7: rng f = [#] T by FUNCT_2:def 3;
take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
A8: dom f = [#] S by FUNCT_2:def 1;
A9: f is one-to-one by A5, FUNCT_2:23;
then g = f " by A5, A7, FUNCT_2:30
.= f " by A6, A9, TOPS_2:def 4 ;
hence f is being_homeomorphism by A9, A7, A8, TOPS_2:def 5; :: thesis: verum