let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)

for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) holds

p in Fr A

let A be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) holds

p in Fr A

let p be Point of (TOP-REAL n); :: thesis: ( n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) implies p in Fr A )

set TRn = TOP-REAL n;

set cTRn = the carrier of (TOP-REAL n);

set CL = cl_Ball ((0. (TOP-REAL n)),1);

set S = Sphere ((0. (TOP-REAL n)),1);

set TS = Tunit_circle n;

assume A1: n > 0 ; :: thesis: ( not p in A or ex r being Real st

( r > 0 & ( for U being open Subset of ((TOP-REAL n) | A) holds

( not p in U or not U c= Ball (p,r) or ex f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | A),(Tunit_circle n) holds

( not h is continuous or not h | (A \ U) = f ) ) ) ) ) ) or p in Fr A )

the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} = {(0. (TOP-REAL n))} ` by SUBSET_1:def 4;

then reconsider cTR0 = the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} as non empty open Subset of (TOP-REAL n) by A1;

set nN = n NormF ;

set TRn0 = (TOP-REAL n) | cTR0;

A2: Int A c= A by TOPS_1:16;

set G = transl (p,(TOP-REAL n));

reconsider I = incl ((TOP-REAL n) | cTR0) as continuous Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TMAP_1:87;

A3: [#] ((TOP-REAL n) | cTR0) = cTR0 by PRE_TOPC:def 5;

A4: (n NormF) | ((TOP-REAL n) | cTR0) = (n NormF) | the carrier of ((TOP-REAL n) | cTR0) by TMAP_1:def 4;

not 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0))

reconsider b = I </> nN0 as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;

A7: Int A in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

set En = Euclid n;

set TM = TopSpaceMetr (Euclid n);

assume that

A8: p in A and

A9: for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ; :: thesis: p in Fr A

reconsider e = p as Point of (Euclid n) by EUCLID:67;

A10: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

then reconsider IA = Int A as Subset of (TopSpaceMetr (Euclid n)) ;

Tunit_circle n = Tcircle ((0. (TOP-REAL n)),1) by TOPREALB:def 7;

then Tunit_circle n = (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) by TOPREALB:def 6;

then A11: [#] (Tunit_circle n) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

assume not p in Fr A ; :: thesis: contradiction

then p in A \ (Fr A) by A8, XBOOLE_0:def 5;

then p in Int A by TOPS_1:40;

then consider r being Real such that

A12: r > 0 and

A13: Ball (e,r) c= IA by A7, A10, PRE_TOPC:def 2, TOPMETR:15;

set r2 = r / 2;

consider U being open Subset of ((TOP-REAL n) | A) such that

A14: p in U and

A15: U c= Ball (p,(r / 2)) and

A16: for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) by A12, A9;

reconsider Sph = Sphere (p,(r / 2)) as non empty Subset of (TOP-REAL n) by A1, A12;

consider au being object such that

A17: au in Sph by XBOOLE_0:def 1;

A18: n in NAT by ORDINAL1:def 12;

A19: Ball (e,r) = Ball (p,r) by TOPREAL9:13;

A20: cl_Ball (p,(r / 2)) c= Ball (p,r) by JORDAN:21, A18, A12, XREAL_1:216;

A21: Sph = (cl_Ball (p,(r / 2))) \ (Ball (p,(r / 2))) by JORDAN:19, A18;

then W: au in cl_Ball (p,(r / 2)) by A17, XBOOLE_0:def 5;

A22: au in IA by W, A20, A19, A13;

reconsider r2 = r / 2 as non zero Real by A12;

reconsider CL2 = cl_Ball (p,r2) as non empty Subset of (TOP-REAL n) by A12;

A23: Sph c= CL2 by A21, XBOOLE_1:36;

[#] ((TOP-REAL n) | CL2) = CL2 by PRE_TOPC:def 5;

then reconsider sph = Sph as non empty Subset of ((TOP-REAL n) | CL2) by A21, XBOOLE_1:36;

A24: ((TOP-REAL n) | CL2) | sph = (TOP-REAL n) | Sph by PRE_TOPC:7, A21, XBOOLE_1:36;

not au in U by A15, A21, A17, XBOOLE_0:def 5;

then reconsider AU = A \ U as non empty Subset of (TOP-REAL n) by A22, A2, XBOOLE_0:def 5;

set TAU = (TOP-REAL n) | AU;

set t = transl ((- p),(TOP-REAL n));

set T = (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU);

A25: [#] ((TOP-REAL n) | AU) = A \ U by PRE_TOPC:def 5;

then A26: dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) = A \ U by FUNCT_2:def 1;

A27: (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU) = (transl ((- p),(TOP-REAL n))) | the carrier of ((TOP-REAL n) | AU) by TMAP_1:def 4;

A28: rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) c= cTR0

A33: [#] ((TOP-REAL n) | Sph) = Sph by PRE_TOPC:def 5;

A34: CL2 c= IA by A20, A19, A13;

A35: CL2 c= A by A2, A20, A19, A13;

A36: dom b = cTR0 by A3, FUNCT_2:def 1;

A37: for p being Point of (TOP-REAL n) st p in cTR0 holds

( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )

A47: [#] (((TOP-REAL n) | CL2) | sph) = sph by PRE_TOPC:def 5;

set m = mlt (r2,(TOP-REAL n));

set M = (mlt (r2,(TOP-REAL n))) | (Tunit_circle n);

reconsider M = (mlt (r2,(TOP-REAL n))) | (Tunit_circle n) as continuous Function of (Tunit_circle n),(TOP-REAL n) by A1;

A48: M = (mlt (r2,(TOP-REAL n))) | the carrier of (Tunit_circle n) by TMAP_1:def 4;

A49: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then reconsider clB = CL2 as Subset of ((TOP-REAL n) | A) by A34, A2, XBOOLE_1:1;

A50: ((TOP-REAL n) | A) | clB = (TOP-REAL n) | CL2 by PRE_TOPC:7, A34, A2, XBOOLE_1:1;

B is continuous by PRE_TOPC:27;

then B * T0 is continuous by TOPS_2:46;

then consider h being Function of ((TOP-REAL n) | A),(Tunit_circle n) such that

A51: h is continuous and

A52: h | (A \ U) = B * T0 by A16;

M * h is continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) by A1, A51, TOPS_2:46;

then reconsider GHM = (transl (p,(TOP-REAL n))) * (M * h) as continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) by TOPS_2:46;

A53: dom h = the carrier of ((TOP-REAL n) | A) by A1, FUNCT_2:def 1;

A54: |.r2.| = r2 by A12, ABSVALUE:def 1;

A55: rng GHM c= Sph

then reconsider ghm = GHM as Function of ((TOP-REAL n) | A),((TOP-REAL n) | Sph) by A55, A49, A33, FUNCT_2:2;

ghm is continuous by PRE_TOPC:27;

then reconsider ghM = ghm | (((TOP-REAL n) | A) | clB) as continuous Function of ((TOP-REAL n) | CL2),(((TOP-REAL n) | CL2) | sph) by A8, A50, A24;

A68: dom ghM = the carrier of ((TOP-REAL n) | CL2) by FUNCT_2:def 1;

A69: ghM = ghm | the carrier of (((TOP-REAL n) | A) | clB) by TMAP_1:def 4, A8;

for w being Point of ((TOP-REAL n) | CL2) st w in Sph holds

ghM . w = w

Ball (p,r2) c= Int CL2 by TOPREAL9:16, TOPS_1:24;

then A85: not CL2 is boundary by A12;

Fr CL2 = Sph by A12, BROUWER2:5;

hence contradiction by A84, A85, A47, BROUWER2:9, BORSUK_1:def 17; :: thesis: verum

for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) holds

p in Fr A

let A be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) holds

p in Fr A

let p be Point of (TOP-REAL n); :: thesis: ( n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) implies p in Fr A )

set TRn = TOP-REAL n;

set cTRn = the carrier of (TOP-REAL n);

set CL = cl_Ball ((0. (TOP-REAL n)),1);

set S = Sphere ((0. (TOP-REAL n)),1);

set TS = Tunit_circle n;

assume A1: n > 0 ; :: thesis: ( not p in A or ex r being Real st

( r > 0 & ( for U being open Subset of ((TOP-REAL n) | A) holds

( not p in U or not U c= Ball (p,r) or ex f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st

( f is continuous & ( for h being Function of ((TOP-REAL n) | A),(Tunit_circle n) holds

( not h is continuous or not h | (A \ U) = f ) ) ) ) ) ) or p in Fr A )

the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} = {(0. (TOP-REAL n))} ` by SUBSET_1:def 4;

then reconsider cTR0 = the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} as non empty open Subset of (TOP-REAL n) by A1;

set nN = n NormF ;

set TRn0 = (TOP-REAL n) | cTR0;

A2: Int A c= A by TOPS_1:16;

set G = transl (p,(TOP-REAL n));

reconsider I = incl ((TOP-REAL n) | cTR0) as continuous Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TMAP_1:87;

A3: [#] ((TOP-REAL n) | cTR0) = cTR0 by PRE_TOPC:def 5;

A4: (n NormF) | ((TOP-REAL n) | cTR0) = (n NormF) | the carrier of ((TOP-REAL n) | cTR0) by TMAP_1:def 4;

not 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0))

proof

then reconsider nN0 = (n NormF) | ((TOP-REAL n) | cTR0) as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by RELAT_1:def 9;
assume
0 in rng ((n NormF) | ((TOP-REAL n) | cTR0))
; :: thesis: contradiction

then consider x being object such that

A5: x in dom ((n NormF) | ((TOP-REAL n) | cTR0)) and

A6: ((n NormF) | ((TOP-REAL n) | cTR0)) . x = 0 by FUNCT_1:def 3;

x in dom (n NormF) by A4, A5, RELAT_1:57;

then reconsider x = x as Element of (TOP-REAL n) ;

reconsider X = x as Element of REAL n by EUCLID:22;

0 = (n NormF) . x by A4, A5, A6, FUNCT_1:47

.= |.X.| by JGRAPH_4:def 1 ;

then x = 0* n by EUCLID:8;

then x = 0. (TOP-REAL n) by EUCLID:70;

then x in {(0. (TOP-REAL n))} by TARSKI:def 1;

hence contradiction by A3, A5, XBOOLE_0:def 5; :: thesis: verum

end;then consider x being object such that

A5: x in dom ((n NormF) | ((TOP-REAL n) | cTR0)) and

A6: ((n NormF) | ((TOP-REAL n) | cTR0)) . x = 0 by FUNCT_1:def 3;

x in dom (n NormF) by A4, A5, RELAT_1:57;

then reconsider x = x as Element of (TOP-REAL n) ;

reconsider X = x as Element of REAL n by EUCLID:22;

0 = (n NormF) . x by A4, A5, A6, FUNCT_1:47

.= |.X.| by JGRAPH_4:def 1 ;

then x = 0* n by EUCLID:8;

then x = 0. (TOP-REAL n) by EUCLID:70;

then x in {(0. (TOP-REAL n))} by TARSKI:def 1;

hence contradiction by A3, A5, XBOOLE_0:def 5; :: thesis: verum

reconsider b = I </> nN0 as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;

A7: Int A in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

set En = Euclid n;

set TM = TopSpaceMetr (Euclid n);

assume that

A8: p in A and

A9: for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ; :: thesis: p in Fr A

reconsider e = p as Point of (Euclid n) by EUCLID:67;

A10: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

then reconsider IA = Int A as Subset of (TopSpaceMetr (Euclid n)) ;

Tunit_circle n = Tcircle ((0. (TOP-REAL n)),1) by TOPREALB:def 7;

then Tunit_circle n = (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) by TOPREALB:def 6;

then A11: [#] (Tunit_circle n) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

assume not p in Fr A ; :: thesis: contradiction

then p in A \ (Fr A) by A8, XBOOLE_0:def 5;

then p in Int A by TOPS_1:40;

then consider r being Real such that

A12: r > 0 and

A13: Ball (e,r) c= IA by A7, A10, PRE_TOPC:def 2, TOPMETR:15;

set r2 = r / 2;

consider U being open Subset of ((TOP-REAL n) | A) such that

A14: p in U and

A15: U c= Ball (p,(r / 2)) and

A16: for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) by A12, A9;

reconsider Sph = Sphere (p,(r / 2)) as non empty Subset of (TOP-REAL n) by A1, A12;

consider au being object such that

A17: au in Sph by XBOOLE_0:def 1;

A18: n in NAT by ORDINAL1:def 12;

A19: Ball (e,r) = Ball (p,r) by TOPREAL9:13;

A20: cl_Ball (p,(r / 2)) c= Ball (p,r) by JORDAN:21, A18, A12, XREAL_1:216;

A21: Sph = (cl_Ball (p,(r / 2))) \ (Ball (p,(r / 2))) by JORDAN:19, A18;

then W: au in cl_Ball (p,(r / 2)) by A17, XBOOLE_0:def 5;

A22: au in IA by W, A20, A19, A13;

reconsider r2 = r / 2 as non zero Real by A12;

reconsider CL2 = cl_Ball (p,r2) as non empty Subset of (TOP-REAL n) by A12;

A23: Sph c= CL2 by A21, XBOOLE_1:36;

[#] ((TOP-REAL n) | CL2) = CL2 by PRE_TOPC:def 5;

then reconsider sph = Sph as non empty Subset of ((TOP-REAL n) | CL2) by A21, XBOOLE_1:36;

A24: ((TOP-REAL n) | CL2) | sph = (TOP-REAL n) | Sph by PRE_TOPC:7, A21, XBOOLE_1:36;

not au in U by A15, A21, A17, XBOOLE_0:def 5;

then reconsider AU = A \ U as non empty Subset of (TOP-REAL n) by A22, A2, XBOOLE_0:def 5;

set TAU = (TOP-REAL n) | AU;

set t = transl ((- p),(TOP-REAL n));

set T = (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU);

A25: [#] ((TOP-REAL n) | AU) = A \ U by PRE_TOPC:def 5;

then A26: dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) = A \ U by FUNCT_2:def 1;

A27: (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU) = (transl ((- p),(TOP-REAL n))) | the carrier of ((TOP-REAL n) | AU) by TMAP_1:def 4;

A28: rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) c= cTR0

proof

then reconsider T0 = (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU) as continuous Function of ((TOP-REAL n) | AU),((TOP-REAL n) | cTR0) by A26, FUNCT_2:2, A3, A25, PRE_TOPC:27;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) or y in cTR0 )

assume y in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) ; :: thesis: y in cTR0

then consider x being object such that

A29: x in dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) and

A30: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x = y by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A29, A26;

A31: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x = (transl ((- p),(TOP-REAL n))) . x by A29, A27, FUNCT_1:47;

A32: (transl ((- p),(TOP-REAL n))) . x = x + (- p) by RLTOPSP1:def 10;

assume not y in cTR0 ; :: thesis: contradiction

then ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x in {(0. (TOP-REAL n))} by A31, XBOOLE_0:def 5, A30;

then x - p = 0. (TOP-REAL n) by TARSKI:def 1, A32, A31;

then x = p by RLVECT_1:21;

hence contradiction by A29, A25, XBOOLE_0:def 5, A14; :: thesis: verum

end;assume y in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) ; :: thesis: y in cTR0

then consider x being object such that

A29: x in dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) and

A30: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x = y by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A29, A26;

A31: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x = (transl ((- p),(TOP-REAL n))) . x by A29, A27, FUNCT_1:47;

A32: (transl ((- p),(TOP-REAL n))) . x = x + (- p) by RLTOPSP1:def 10;

assume not y in cTR0 ; :: thesis: contradiction

then ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x in {(0. (TOP-REAL n))} by A31, XBOOLE_0:def 5, A30;

then x - p = 0. (TOP-REAL n) by TARSKI:def 1, A32, A31;

then x = p by RLVECT_1:21;

hence contradiction by A29, A25, XBOOLE_0:def 5, A14; :: thesis: verum

A33: [#] ((TOP-REAL n) | Sph) = Sph by PRE_TOPC:def 5;

A34: CL2 c= IA by A20, A19, A13;

A35: CL2 c= A by A2, A20, A19, A13;

A36: dom b = cTR0 by A3, FUNCT_2:def 1;

A37: for p being Point of (TOP-REAL n) st p in cTR0 holds

( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )

proof

rng b c= Sphere ((0. (TOP-REAL n)),1)
let p be Point of (TOP-REAL n); :: thesis: ( p in cTR0 implies ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) )

A38: |.(1 / |.p.|).| = 1 / |.p.| by ABSVALUE:def 1;

assume A39: p in cTR0 ; :: thesis: ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )

then A40: I . p = p by A3, TMAP_1:84;

A41: nN0 . p = (n NormF) . p by A39, A3, A4, FUNCT_1:49;

thus b . p = (I . p) (/) (nN0 . p) by A36, A39, VALUED_2:72

.= p (/) |.p.| by A41, A40, JGRAPH_4:def 1

.= (1 / |.p.|) * p by VALUED_2:def 32 ; :: thesis: |.((1 / |.p.|) * p).| = 1

A42: p <> 0. (TOP-REAL n) by A39, ZFMISC_1:56;

thus |.((1 / |.p.|) * p).| = |.(1 / |.p.|).| * |.p.| by TOPRNS_1:7

.= 1 by A38, A42, TOPRNS_1:24, XCMPLX_1:87 ; :: thesis: verum

end;A38: |.(1 / |.p.|).| = 1 / |.p.| by ABSVALUE:def 1;

assume A39: p in cTR0 ; :: thesis: ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )

then A40: I . p = p by A3, TMAP_1:84;

A41: nN0 . p = (n NormF) . p by A39, A3, A4, FUNCT_1:49;

thus b . p = (I . p) (/) (nN0 . p) by A36, A39, VALUED_2:72

.= p (/) |.p.| by A41, A40, JGRAPH_4:def 1

.= (1 / |.p.|) * p by VALUED_2:def 32 ; :: thesis: |.((1 / |.p.|) * p).| = 1

A42: p <> 0. (TOP-REAL n) by A39, ZFMISC_1:56;

thus |.((1 / |.p.|) * p).| = |.(1 / |.p.|).| * |.p.| by TOPRNS_1:7

.= 1 by A38, A42, TOPRNS_1:24, XCMPLX_1:87 ; :: thesis: verum

proof

then reconsider B = b as Function of ((TOP-REAL n) | cTR0),(Tunit_circle n) by A3, A11, A36, FUNCT_2:2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng b or y in Sphere ((0. (TOP-REAL n)),1) )

assume y in rng b ; :: thesis: y in Sphere ((0. (TOP-REAL n)),1)

then consider x being object such that

A43: x in dom b and

A44: b . x = y by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A36, A43;

A45: |.((1 / |.x.|) * x).| = 1 by A3, A37, A43;

A46: ((1 / |.x.|) * x) - (0. (TOP-REAL n)) = (1 / |.x.|) * x by RLVECT_1:13;

y = (1 / |.x.|) * x by A3, A37, A43, A44;

hence y in Sphere ((0. (TOP-REAL n)),1) by A46, A45; :: thesis: verum

end;assume y in rng b ; :: thesis: y in Sphere ((0. (TOP-REAL n)),1)

then consider x being object such that

A43: x in dom b and

A44: b . x = y by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A36, A43;

A45: |.((1 / |.x.|) * x).| = 1 by A3, A37, A43;

A46: ((1 / |.x.|) * x) - (0. (TOP-REAL n)) = (1 / |.x.|) * x by RLVECT_1:13;

y = (1 / |.x.|) * x by A3, A37, A43, A44;

hence y in Sphere ((0. (TOP-REAL n)),1) by A46, A45; :: thesis: verum

A47: [#] (((TOP-REAL n) | CL2) | sph) = sph by PRE_TOPC:def 5;

set m = mlt (r2,(TOP-REAL n));

set M = (mlt (r2,(TOP-REAL n))) | (Tunit_circle n);

reconsider M = (mlt (r2,(TOP-REAL n))) | (Tunit_circle n) as continuous Function of (Tunit_circle n),(TOP-REAL n) by A1;

A48: M = (mlt (r2,(TOP-REAL n))) | the carrier of (Tunit_circle n) by TMAP_1:def 4;

A49: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

then reconsider clB = CL2 as Subset of ((TOP-REAL n) | A) by A34, A2, XBOOLE_1:1;

A50: ((TOP-REAL n) | A) | clB = (TOP-REAL n) | CL2 by PRE_TOPC:7, A34, A2, XBOOLE_1:1;

B is continuous by PRE_TOPC:27;

then B * T0 is continuous by TOPS_2:46;

then consider h being Function of ((TOP-REAL n) | A),(Tunit_circle n) such that

A51: h is continuous and

A52: h | (A \ U) = B * T0 by A16;

M * h is continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) by A1, A51, TOPS_2:46;

then reconsider GHM = (transl (p,(TOP-REAL n))) * (M * h) as continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) by TOPS_2:46;

A53: dom h = the carrier of ((TOP-REAL n) | A) by A1, FUNCT_2:def 1;

A54: |.r2.| = r2 by A12, ABSVALUE:def 1;

A55: rng GHM c= Sph

proof

dom GHM = A
by A49, FUNCT_2:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng GHM or y in Sph )

assume y in rng GHM ; :: thesis: y in Sph

then consider q being object such that

A56: q in dom GHM and

A57: GHM . q = y by FUNCT_1:def 3;

A58: y = (transl (p,(TOP-REAL n))) . ((M * h) . q) by A56, A57, FUNCT_1:12;

A59: q in A by A56, A49;

A60: q in dom (M * h) by A56, FUNCT_1:11;

then A61: q in dom h by FUNCT_1:11;

A62: (M * h) . q = M . (h . q) by A60, FUNCT_1:12;

A63: h . q in dom M by A60, FUNCT_1:11;

reconsider q = q as Point of (TOP-REAL n) by A59;

h . q in Sphere ((0. (TOP-REAL n)),1) by A63, A11;

then reconsider hq = h . q as Point of (TOP-REAL n) ;

A64: (mlt (r2,(TOP-REAL n))) . (h . q) = r2 * hq by RLTOPSP1:def 13;

M . (h . q) = (mlt (r2,(TOP-REAL n))) . (h . q) by A63, A48, FUNCT_1:47;

then A65: y = p + (r2 * hq) by A58, A62, A64, RLTOPSP1:def 10;

A66: (p + (r2 * hq)) - p = (r2 * hq) + (p - p) by RLVECT_1:28

.= (r2 * hq) + (0. (TOP-REAL n)) by RLVECT_1:15

.= r2 * hq by RLVECT_1:def 4 ;

A67: h . q in rng h by FUNCT_1:def 3, A61;

|.(r2 * hq).| = |.r2.| * |.hq.| by EUCLID:11

.= |.r2.| * 1 by A67, A11, TOPREAL9:12 ;

hence y in Sph by A66, A65, A54; :: thesis: verum

end;assume y in rng GHM ; :: thesis: y in Sph

then consider q being object such that

A56: q in dom GHM and

A57: GHM . q = y by FUNCT_1:def 3;

A58: y = (transl (p,(TOP-REAL n))) . ((M * h) . q) by A56, A57, FUNCT_1:12;

A59: q in A by A56, A49;

A60: q in dom (M * h) by A56, FUNCT_1:11;

then A61: q in dom h by FUNCT_1:11;

A62: (M * h) . q = M . (h . q) by A60, FUNCT_1:12;

A63: h . q in dom M by A60, FUNCT_1:11;

reconsider q = q as Point of (TOP-REAL n) by A59;

h . q in Sphere ((0. (TOP-REAL n)),1) by A63, A11;

then reconsider hq = h . q as Point of (TOP-REAL n) ;

A64: (mlt (r2,(TOP-REAL n))) . (h . q) = r2 * hq by RLTOPSP1:def 13;

M . (h . q) = (mlt (r2,(TOP-REAL n))) . (h . q) by A63, A48, FUNCT_1:47;

then A65: y = p + (r2 * hq) by A58, A62, A64, RLTOPSP1:def 10;

A66: (p + (r2 * hq)) - p = (r2 * hq) + (p - p) by RLVECT_1:28

.= (r2 * hq) + (0. (TOP-REAL n)) by RLVECT_1:15

.= r2 * hq by RLVECT_1:def 4 ;

A67: h . q in rng h by FUNCT_1:def 3, A61;

|.(r2 * hq).| = |.r2.| * |.hq.| by EUCLID:11

.= |.r2.| * 1 by A67, A11, TOPREAL9:12 ;

hence y in Sph by A66, A65, A54; :: thesis: verum

then reconsider ghm = GHM as Function of ((TOP-REAL n) | A),((TOP-REAL n) | Sph) by A55, A49, A33, FUNCT_2:2;

ghm is continuous by PRE_TOPC:27;

then reconsider ghM = ghm | (((TOP-REAL n) | A) | clB) as continuous Function of ((TOP-REAL n) | CL2),(((TOP-REAL n) | CL2) | sph) by A8, A50, A24;

A68: dom ghM = the carrier of ((TOP-REAL n) | CL2) by FUNCT_2:def 1;

A69: ghM = ghm | the carrier of (((TOP-REAL n) | A) | clB) by TMAP_1:def 4, A8;

for w being Point of ((TOP-REAL n) | CL2) st w in Sph holds

ghM . w = w

proof

then A84:
ghM is being_a_retraction
by BORSUK_1:def 16, A33, A24;
let w be Point of ((TOP-REAL n) | CL2); :: thesis: ( w in Sph implies ghM . w = w )

assume A70: w in Sph ; :: thesis: ghM . w = w

then reconsider q = w as Point of (TOP-REAL n) ;

A71: w in CL2 by A70, A23;

w in A by A35, A70, A23;

then A72: q in dom GHM by A49, FUNCT_2:def 1;

then A73: q in dom (M * h) by FUNCT_1:11;

then A74: (M * h) . q = M . (h . q) by FUNCT_1:12;

not q in U by A70, A21, XBOOLE_0:def 5, A15;

then A75: q in A \ U by A71, A35, XBOOLE_0:def 5;

then q in (A \ U) /\ (dom h) by A71, A35, A53, A49, XBOOLE_0:def 4;

then A76: q in dom (B * T0) by A52, RELAT_1:61;

then A77: (B * T0) . q = B . (T0 . q) by FUNCT_1:12;

A78: h . q in dom M by A73, FUNCT_1:11;

then A79: M . (h . q) = (mlt (r2,(TOP-REAL n))) . (h . q) by A48, FUNCT_1:47;

(transl ((- p),(TOP-REAL n))) . q = q + (- p) by RLTOPSP1:def 10;

then A80: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . q = q - p by A26, A27, A75, FUNCT_1:47;

q in dom T0 by A76, FUNCT_1:11;

then A81: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . q in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) by FUNCT_1:def 3;

h . q in Sphere ((0. (TOP-REAL n)),1) by A78, A11;

then reconsider hq = h . q as Point of (TOP-REAL n) ;

ghM . q = ghm . q by A68, A69, FUNCT_1:47;

then A82: ghM . q = (transl (p,(TOP-REAL n))) . ((M * h) . q) by A72, FUNCT_1:12;

hq = (B * T0) . q by A76, A52, FUNCT_1:47;

then A83: hq = (1 / |.(q - p).|) * (q - p) by A80, A77, A37, A81, A28;

(mlt (r2,(TOP-REAL n))) . (h . q) = r2 * hq by RLTOPSP1:def 13

.= r2 * ((1 / r2) * (q - p)) by A83, A70, TOPREAL9:9

.= (r2 * (1 / r2)) * (q - p) by RLVECT_1:def 7

.= 1 * (q - p) by XCMPLX_1:106

.= q - p by RLVECT_1:def 8 ;

then ghM . w = p + (q - p) by A82, A74, A79, RLTOPSP1:def 10

.= q + ((- p) + p) by RLVECT_1:def 3

.= q + (0. (TOP-REAL n)) by RLVECT_1:def 10

.= q by RLVECT_1:4 ;

hence ghM . w = w ; :: thesis: verum

end;assume A70: w in Sph ; :: thesis: ghM . w = w

then reconsider q = w as Point of (TOP-REAL n) ;

A71: w in CL2 by A70, A23;

w in A by A35, A70, A23;

then A72: q in dom GHM by A49, FUNCT_2:def 1;

then A73: q in dom (M * h) by FUNCT_1:11;

then A74: (M * h) . q = M . (h . q) by FUNCT_1:12;

not q in U by A70, A21, XBOOLE_0:def 5, A15;

then A75: q in A \ U by A71, A35, XBOOLE_0:def 5;

then q in (A \ U) /\ (dom h) by A71, A35, A53, A49, XBOOLE_0:def 4;

then A76: q in dom (B * T0) by A52, RELAT_1:61;

then A77: (B * T0) . q = B . (T0 . q) by FUNCT_1:12;

A78: h . q in dom M by A73, FUNCT_1:11;

then A79: M . (h . q) = (mlt (r2,(TOP-REAL n))) . (h . q) by A48, FUNCT_1:47;

(transl ((- p),(TOP-REAL n))) . q = q + (- p) by RLTOPSP1:def 10;

then A80: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . q = q - p by A26, A27, A75, FUNCT_1:47;

q in dom T0 by A76, FUNCT_1:11;

then A81: ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . q in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) by FUNCT_1:def 3;

h . q in Sphere ((0. (TOP-REAL n)),1) by A78, A11;

then reconsider hq = h . q as Point of (TOP-REAL n) ;

ghM . q = ghm . q by A68, A69, FUNCT_1:47;

then A82: ghM . q = (transl (p,(TOP-REAL n))) . ((M * h) . q) by A72, FUNCT_1:12;

hq = (B * T0) . q by A76, A52, FUNCT_1:47;

then A83: hq = (1 / |.(q - p).|) * (q - p) by A80, A77, A37, A81, A28;

(mlt (r2,(TOP-REAL n))) . (h . q) = r2 * hq by RLTOPSP1:def 13

.= r2 * ((1 / r2) * (q - p)) by A83, A70, TOPREAL9:9

.= (r2 * (1 / r2)) * (q - p) by RLVECT_1:def 7

.= 1 * (q - p) by XCMPLX_1:106

.= q - p by RLVECT_1:def 8 ;

then ghM . w = p + (q - p) by A82, A74, A79, RLTOPSP1:def 10

.= q + ((- p) + p) by RLVECT_1:def 3

.= q + (0. (TOP-REAL n)) by RLVECT_1:def 10

.= q by RLVECT_1:4 ;

hence ghM . w = w ; :: thesis: verum

Ball (p,r2) c= Int CL2 by TOPREAL9:16, TOPS_1:24;

then A85: not CL2 is boundary by A12;

Fr CL2 = Sph by A12, BROUWER2:5;

hence contradiction by A84, A85, A47, BROUWER2:9, BORSUK_1:def 17; :: thesis: verum