let S, T be being_simple_closed_curve SubSpace of TOP-REAL 2; :: thesis: S,T are_homeomorphic
TopStruct(# the carrier of S,the topology of S #), TopStruct(# the carrier of T,the topology of T #) are_homeomorphic
proof
reconsider A = the
carrier of
TopStruct(# the
carrier of
S,the
topology of
S #) as
Simple_closed_curve by Def5;
reconsider B = the
carrier of
TopStruct(# the
carrier of
T,the
topology of
T #) as
Simple_closed_curve by Def5;
consider f being
Function of
((TOP-REAL 2) | R^2-unit_square ),
((TOP-REAL 2) | A) such that A1:
f is
being_homeomorphism
by TOPREAL2:def 1;
consider g being
Function of
((TOP-REAL 2) | R^2-unit_square ),
((TOP-REAL 2) | B) such that A2:
g is
being_homeomorphism
by TOPREAL2:def 1;
A3:
TopStruct(# the
carrier of
S,the
topology of
S #) is
strict SubSpace of
TOP-REAL 2
by TMAP_1:11;
[#] TopStruct(# the
carrier of
S,the
topology of
S #)
= A
;
then A4:
TopStruct(# the
carrier of
S,the
topology of
S #)
= (TOP-REAL 2) | A
by A3, PRE_TOPC:def 10;
A5:
TopStruct(# the
carrier of
T,the
topology of
T #) is
strict SubSpace of
TOP-REAL 2
by TMAP_1:11;
[#] TopStruct(# the
carrier of
T,the
topology of
T #)
= B
;
then A6:
TopStruct(# the
carrier of
T,the
topology of
T #)
= (TOP-REAL 2) | B
by A5, PRE_TOPC:def 10;
then reconsider h =
g * (f " ) as
Function of
TopStruct(# the
carrier of
S,the
topology of
S #),
TopStruct(# the
carrier of
T,the
topology of
T #)
by A4;
take
h
;
:: according to T_0TOPSP:def 1 :: thesis: h is being_homeomorphism
f " is
being_homeomorphism
by A1, TOPS_2:70;
hence
h is
being_homeomorphism
by A2, A4, A6, TOPS_2:71;
:: thesis: verum
end;
hence
S,T are_homeomorphic
by TOPREALA:36; :: thesis: verum