let n be Nat; :: thesis: for A being non empty convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
set T = TOP-REAL n;
set cB = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
A1: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
then reconsider s = Sphere ((0. (TOP-REAL n)),1) as Subset of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by TOPREAL9:17;
A2: (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s by PRE_TOPC:7, TOPREAL9:17;
let A be non empty convex Subset of (TOP-REAL n); :: thesis: ( A is compact & not A is boundary implies for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A )
assume A3: ( A is compact & not A is boundary ) ; :: thesis: for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
A4: ( [#] ((TOP-REAL n) | A) = A & Fr A c= A ) by A3, PRE_TOPC:def 5, TOPS_1:35;
let FR be non empty SubSpace of (TOP-REAL n) | A; :: thesis: ( [#] FR = Fr A implies not FR is_a_retract_of (TOP-REAL n) | A )
assume A5: [#] FR = Fr A ; :: thesis: not FR is_a_retract_of (TOP-REAL n) | A
n > 0 then reconsider Ts = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s as non empty SubSpace of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) ;
assume FR is_a_retract_of (TOP-REAL n) | A ; :: thesis: contradiction
then consider F being continuous Function of ((TOP-REAL n) | A),FR such that
A7: F is being_a_retraction ;
reconsider f = F as Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) by A5, A4, FUNCT_2:7;
A8: f is continuous by PRE_TOPC:26;
A9: rng F c= Fr A by A5;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set TN = TOP-REAL N;
A10: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
( (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) = Tdisk ((0. (TOP-REAL N)),1) & (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = Tcircle ((0. (TOP-REAL N)),1) ) by TOPREALB:def 6;
then A11: not Ts is_a_retract_of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) by A2, Lm6;
not cl_Ball ((0. (TOP-REAL n)),1) is boundary by Lm5;
then consider h being Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),((TOP-REAL n) | A) such that
A12: h is being_homeomorphism and
A13: h .: (Fr (cl_Ball ((0. (TOP-REAL n)),1))) = Fr A by A3, Th7;
A14: dom h = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A12, TOPS_2:def 5;
rng ((h ") * f) = ((h ") * f) .: (dom ((h ") * f)) by RELAT_1:113;
then A15: rng ((h ") * f) c= ((h ") * f) .: (dom f) by RELAT_1:25, RELAT_1:123;
reconsider H = h as Function ;
A16: Fr (cl_Ball ((0. (TOP-REAL n)),1)) = Sphere ((0. (TOP-REAL n)),1) by Th5;
rng h = [#] ((TOP-REAL n) | A) by A12, TOPS_2:def 5;
then A17: (h ") .: (Fr A) = h " (Fr A) by A12, A4, TOPS_2:55
.= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A12, A13, A1, A14, FUNCT_1:94, TOPS_1:35 ;
((h ") * f) .: (dom f) = (h ") .: (f .: (dom f)) by RELAT_1:126
.= (h ") .: (rng f) by RELAT_1:113 ;
then ((h ") * f) .: (dom f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A17, A9, RELAT_1:123;
then ( rng (((h ") * f) * h) c= rng ((h ") * f) & rng ((h ") * f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) ) by A15, RELAT_1:26;
then rng (((h ") * f) * h) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) ;
then reconsider hfh = ((h ") * f) * h as Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),Ts by A2, A16, A10, FUNCT_2:6;
h " is continuous by A12, TOPS_2:def 5;
then hfh is continuous by A12, A8, PRE_TOPC:27;
then not hfh is being_a_retraction by A11;
then consider x being Point of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) such that
A18: x in Sphere ((0. (TOP-REAL n)),1) and
A19: hfh . x <> x by A2, A10;
set hx = h . x;
A20: dom hfh = the carrier of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by FUNCT_2:def 1;
then A21: hfh . x = ((h ") * f) . (h . x) by FUNCT_1:12;
x in dom h by A20, FUNCT_1:11;
then A22: h . x in the carrier of FR by A5, A13, A16, A18, FUNCT_1:def 6;
h . x in dom ((h ") * f) by A20, FUNCT_1:11;
then A23: ((h ") * f) . (h . x) = (h ") . (f . (h . x)) by FUNCT_1:12;
A24: H " = h " by A12, TOPS_2:def 4;
(H ") . (h . x) = x by A12, A14, FUNCT_1:34;
hence contradiction by A7, A24, A19, A21, A23, A22; :: thesis: verum