let n be Nat; for A, B being convex Subset of (TOP-REAL n) st A is compact & not A is boundary & B is compact & not B is boundary holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism & h .: (Fr A) = Fr B )
set T = TOP-REAL n;
let A, B be convex Subset of (TOP-REAL n); ( A is compact & not A is boundary & B is compact & not B is boundary implies ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism & h .: (Fr A) = Fr B ) )
assume that
A1:
( A is compact & not A is boundary )
and
A2:
( B is compact & not B is boundary )
; ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism & h .: (Fr A) = Fr B )
A3:
( not A is empty & not B is empty )
by A1, A2;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set TN = TOP-REAL N;
consider hA being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL N)),1)) such that
A4:
hA is being_homeomorphism
and
A5:
hA .: (Fr A) = Sphere ((0. (TOP-REAL n)),1)
by A1, Th6;
consider hB being Function of ((TOP-REAL n) | B),(Tdisk ((0. (TOP-REAL N)),1)) such that
A6:
hB is being_homeomorphism
and
A7:
hB .: (Fr B) = Sphere ((0. (TOP-REAL n)),1)
by A2, Th6;
reconsider h = (hB ") * hA as Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) ;
take
h
; ( h is being_homeomorphism & h .: (Fr A) = Fr B )
hB " is being_homeomorphism
by A6, TOPS_2:56;
hence
h is being_homeomorphism
by A3, A4, TOPS_2:57; h .: (Fr A) = Fr B
A8:
rng hB = [#] (Tdisk ((0. (TOP-REAL N)),1))
by A6, TOPS_2:def 5;
dom hB = [#] ((TOP-REAL n) | B)
by A6, TOPS_2:def 5;
then A9:
dom hB = B
by PRE_TOPC:def 5;
the carrier of (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1)
by BROUWER:3;
then A10:
Sphere ((0. (TOP-REAL n)),1) is Subset of (Tdisk ((0. (TOP-REAL N)),1))
by TOPREAL9:17;
thus h .: (Fr A) =
(hB ") .: (Sphere ((0. (TOP-REAL n)),1))
by A5, RELAT_1:126
.=
hB " (Sphere ((0. (TOP-REAL n)),1))
by A6, A8, A10, TOPS_2:55
.=
Fr B
by A2, A6, A7, A9, FUNCT_1:94, TOPS_1:35
; verum