let n be Element of NAT ; :: thesis: for X being non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1) st X = Tcircle ((0. (TOP-REAL n)),1) holds
not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
set TR = TOP-REAL n;
set Td = Tdisk ((0. (TOP-REAL n)),1);
A1: Sphere ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1) by TOPREAL9:17;
set M = mlt ((- jj),(TOP-REAL n));
let X be non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1); :: thesis: ( X = Tcircle ((0. (TOP-REAL n)),1) implies not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) )
assume A2: X = Tcircle ((0. (TOP-REAL n)),1) ; :: thesis: not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
A3: the carrier of X = Sphere ((0. (TOP-REAL n)),1) by A2, TOPREALB:9;
assume X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) ; :: thesis: contradiction
then consider F being continuous Function of (Tdisk ((0. (TOP-REAL n)),1)),X such that
A4: F is being_a_retraction ;
A5: the carrier of (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by BROUWER:3;
then reconsider f = F as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A3, A1, FUNCT_2:7;
set Mf = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f;
A6: (mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1)) = (mlt ((- jj),(TOP-REAL n))) | the carrier of (Tdisk ((0. (TOP-REAL n)),1)) by TMAP_1:def 4;
A7: rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= Sphere ((0. (TOP-REAL n)),1)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) or y in Sphere ((0. (TOP-REAL n)),1) )
assume y in rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) ; :: thesis: y in Sphere ((0. (TOP-REAL n)),1)
then consider x being object such that
A8: x in dom (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) and
A9: (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) . x = y by FUNCT_1:def 3;
A10: f . x in dom ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) by A8, FUNCT_1:11;
then f . x in dom (mlt ((- jj),(TOP-REAL n))) by A6, RELAT_1:57;
then reconsider fx = f . x as Point of (TOP-REAL n) ;
x in dom f by A8, FUNCT_1:11;
then f . x in rng F by FUNCT_1:def 3;
then A11: 1 = |.fx.| by A3, TOPREAL9:12
.= |.(- fx).| by EUCLID:10
.= |.((- fx) - (0. (TOP-REAL n))).| ;
y = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . (f . x) by A8, A9, FUNCT_1:12;
then y = (mlt ((- jj),(TOP-REAL n))) . (f . x) by A6, A10, FUNCT_1:47;
then y = (- 1) * fx by RLTOPSP1:def 13
.= - fx by RLVECT_1:16 ;
hence y in Sphere ((0. (TOP-REAL n)),1) by A11; :: thesis: verum

end;

then rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= cl_Ball ((0. (TOP-REAL n)),1) by A1;
then reconsider MF = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A5, FUNCT_2:6;
A12: not cl_Ball ((0. (TOP-REAL n)),1) is boundary by Lm5;
f is continuous by PRE_TOPC:26;
then MF is continuous by PRE_TOPC:27;
then MF is with_fixpoint by A12, Th8;
then consider p being object such that
A13: p is_a_fixpoint_of MF by ABIAN:def 5;
A14: p in dom MF by A13, ABIAN:def 3;
A15: p = MF . p by A13, ABIAN:def 3;
then A16: p in rng MF by A14, FUNCT_1:def 3;
then reconsider p = p as Point of (TOP-REAL n) by A7;
A17: f . p = p by A4, A3, A7, A16;
then A18: p in dom ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) by A14, FUNCT_1:11;
p = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . p by A14, A15, A17, FUNCT_1:12;
then p = (mlt ((- jj),(TOP-REAL n))) . p by A6, A18, FUNCT_1:47;
then p = (- 1) * p by RLTOPSP1:def 13
.= - p by RLVECT_1:16 ;
then A19: p = 0. (TOP-REAL n) by RLVECT_1:19;
|.p.| = 1 by A7, A16, TOPREAL9:12;
hence contradiction by A19, TOPRNS_1:23; :: thesis: verum