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
by T_0TOPSP:def 1;
reconsider f =
f as
continuous Function of
S,
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 )
(
f is
one-to-one &
rng f = [#] T &
dom f = [#] S )
by A1, TOPS_2:def 5;
hence
(
f * g = id T &
g * f = id S )
by TOPS_2:65;
:: thesis: verum
end;
given f being continuous Function of S,T, g being continuous Function of T,S such that A2:
( f * g = id T & g * f = id S )
; :: thesis: S,T are_homeomorphic
take
f
; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
A3:
( f is one-to-one & rng f = [#] T & dom f = [#] S )
by A2, FUNCT_2:29, FUNCT_2:def 1;
then g =
f "
by A2, FUNCT_2:36
.=
f "
by A3, TOPS_2:def 4
;
hence
f is being_homeomorphism
by A3, TOPS_2:def 5; :: thesis: verum