let n be Element of NAT ; :: thesis: for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
set TRn = TOP-REAL n;
let A be convex Subset of (TOP-REAL n); :: thesis: ( A is compact & not A is boundary implies ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) )
assume A1: ( A is compact & not A is boundary ) ; :: thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
Int A <> {} by A1, TOPS_1:48;
then consider p being object such that
A2: p in Int A by XBOOLE_0:def 1;
set TRnA = (TOP-REAL n) | A;
reconsider p = p as Point of (TOP-REAL n) by A2;
A3: Int A c= A by TOPS_1:16;
A4: not A is empty by A2;

per cases ( n = 0 or n > 0 ) ;

suppose A5: n = 0 ; :: thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )

set T = Tdisk ((0. (TOP-REAL n)),1);
A6: {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by A5, EUCLID:22, EUCLID:77;
then A7: A = {(0. (TOP-REAL n))} by A4, ZFMISC_1:33;
then reconsider I = id ((TOP-REAL n) | A) as Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) by A6, ZFMISC_1:33;
take I ; :: thesis: ( I is being_homeomorphism & I .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
A8: Fr A = A \ (Int A) by A5, TOPS_1:43;
A9: Sphere ((0. (TOP-REAL n)),1) = {}

proof

assume Sphere ((0. (TOP-REAL n)),1) <> {} ; :: thesis: contradiction
then Sphere ((0. (TOP-REAL n)),1) = A by A6, A7, ZFMISC_1:33;
then |.(0. (TOP-REAL n)).| = 1 by A6, A7, TOPREAL9:12;
hence contradiction by TOPRNS_1:23; :: thesis: verum

end;

Int A = A by A2, A3, A7, ZFMISC_1:33;
then A10: Fr A = {} by A8, XBOOLE_1:37;
Tdisk ((0. (TOP-REAL n)),1) = (TOP-REAL n) | A by A6, A7, ZFMISC_1:33;
hence ( I is being_homeomorphism & I .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) by A10, A9; :: thesis: verum

end;

suppose A11: n > 0 ; :: thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )

set T = transl ((- p),(TOP-REAL n));
set TA = (transl ((- p),(TOP-REAL n))) .: A;
A12: (transl ((- p),(TOP-REAL n))) .: A = (- p) + A by RLTOPSP1:33;
then A13: ( 0. (TOP-REAL n) = 0* n & (transl ((- p),(TOP-REAL n))) .: A is convex ) by CONVEX1:7, EUCLID:70;
reconsider TT = (transl ((- p),(TOP-REAL n))) | A as Function of ((TOP-REAL n) | A),((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)) by JORDAN24:12;
A14: TT .: (Int A) = (transl ((- p),(TOP-REAL n))) .: (Int A) by RELAT_1:129, TOPS_1:16;
0. (TOP-REAL n) = (- p) + p by RLVECT_1:5;
then A15: 0. (TOP-REAL n) in { ((- p) + q) where q is Element of (TOP-REAL n) : q in Int A } by A2;
Int ((transl ((- p),(TOP-REAL n))) .: A) = (- p) + (Int A) by A12, RLTOPSP1:37;
then 0. (TOP-REAL n) in Int ((transl ((- p),(TOP-REAL n))) .: A) by A15, RUSUB_4:def 8;
then consider h being Function of ((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)),(Tdisk ((0. (TOP-REAL n)),1)) such that
A16: h is being_homeomorphism and
A17: h .: (Fr ((transl ((- p),(TOP-REAL n))) .: A)) = Sphere ((0. (TOP-REAL n)),1) by A1, A11, A12, A13, Lm4;
reconsider hTT = h * TT as Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) by A4;
take hTT ; :: thesis: ( hTT is being_homeomorphism & hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
A18: Int ((transl ((- p),(TOP-REAL n))) .: A) = (- p) + (Int A) by A12, RLTOPSP1:37
.= (transl ((- p),(TOP-REAL n))) .: (Int A) by RLTOPSP1:33 ;
A19: TT is being_homeomorphism by JORDAN24:14;
then dom TT = [#] ((TOP-REAL n) | A) by TOPS_2:def 5;
then A20: dom TT = A by PRE_TOPC:def 5;
thus hTT is being_homeomorphism by A4, A16, A19, TOPS_2:57; :: thesis: hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1)
rng TT = [#] ((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)) by A19, TOPS_2:def 5;
then A21: rng TT = (transl ((- p),(TOP-REAL n))) .: A by PRE_TOPC:def 5;
Fr A = A \ (Int A) by A1, TOPS_1:43;
then A22: TT .: (Fr A) = (TT .: A) \ (TT .: (Int A)) by A19, FUNCT_1:64;
Fr ((transl ((- p),(TOP-REAL n))) .: A) = ((transl ((- p),(TOP-REAL n))) .: A) \ (Int ((transl ((- p),(TOP-REAL n))) .: A)) by A1, A12, TOPS_1:43
.= TT .: (Fr A) by A18, A22, A20, A21, A14, RELAT_1:113 ;
hence hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) by A17, RELAT_1:126; :: thesis: verum

end;

end;