let S, T be non empty TopSpace; ( 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 ( 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
;
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;
ex g being continuous Function of T,S st
( f * g = id T & g * f = id S )take g =
g;
( f * g = id T & g * f = id S )A3:
dom f = [#] S
by A1, TOPS_2:def 5;
f is
V7()
by A1, TOPS_2:def 5;
hence
(
f * g = id T &
g * f = id S )
by A2, A3, TOPS_2:52;
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
; 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
; T_0TOPSP:def 1 f is being_homeomorphism
A8:
dom f = [#] S
by FUNCT_2:def 1;
A9:
f is V7()
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; verum