let n be Nat; :: thesis: for A being Subset of ()
for p being Point of () st n > 0 & p in A & ( for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) ) ) holds
p in Fr A

let A be Subset of (); :: thesis: for p being Point of () st n > 0 & p in A & ( for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) ) ) holds
p in Fr A

let p be Point of (); :: thesis: ( n > 0 & p in A & ( for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) ) ) implies p in Fr A )

set TRn = TOP-REAL n;
set cTRn = the carrier of ();
set CL = cl_Ball ((0. ()),1);
set S = Sphere ((0. ()),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 (() | A) holds
( not p in U or not U c= Ball (p,r) or ex f being Function of (() | (A \ U)),() st
( f is continuous & ( for h being Function of (() | A),() holds
( not h is continuous or not h | (A \ U) = f ) ) ) ) ) ) or p in Fr A )

the carrier of () \ {(0. ())} = {(0. ())} ` by SUBSET_1:def 4;
then reconsider cTR0 = the carrier of () \ {(0. ())} as non empty open Subset of () by A1;
set nN = n NormF ;
set TRn0 = () | cTR0;
A2: Int A c= A by TOPS_1:16;
set G = transl (p,());
reconsider I = incl (() | cTR0) as continuous Function of (() | cTR0),() by TMAP_1:87;
A3: [#] (() | cTR0) = cTR0 by PRE_TOPC:def 5;
A4: (n NormF) | (() | cTR0) = () | the carrier of (() | cTR0) by TMAP_1:def 4;
not 0 in rng (() | (() | cTR0))
proof
assume 0 in rng (() | (() | cTR0)) ; :: thesis: contradiction
then consider x being object such that
A5: x in dom (() | (() | cTR0)) and
A6: ((n NormF) | (() | cTR0)) . x = 0 by FUNCT_1:def 3;
x in dom () by ;
then reconsider x = x as Element of () ;
reconsider X = x as Element of REAL n by EUCLID:22;
0 = () . x by
.= |.X.| by JGRAPH_4:def 1 ;
then x = 0* n by EUCLID:8;
then x = 0. () by EUCLID:70;
then x in {(0. ())} by TARSKI:def 1;
hence contradiction by A3, A5, XBOOLE_0:def 5; :: thesis: verum
end;
then reconsider nN0 = () | (() | cTR0) as non-empty continuous Function of (() | cTR0),R^1 by RELAT_1:def 9;
reconsider b = I </> nN0 as Function of (() | cTR0),() by TOPREALC:46;
A7: Int A in the topology of () by PRE_TOPC:def 2;
set En = Euclid n;
set TM = TopSpaceMetr ();
assume that
A8: p in A and
A9: for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) ) ; :: thesis: p in Fr A
reconsider e = p as Point of () by EUCLID:67;
A10: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider IA = Int A as Subset of () ;
Tunit_circle n = Tcircle ((0. ()),1) by TOPREALB:def 7;
then Tunit_circle n = () | (Sphere ((0. ()),1)) by TOPREALB:def 6;
then A11: [#] () = Sphere ((0. ()),1) by PRE_TOPC:def 5;
assume not p in Fr A ; :: thesis: contradiction
then p in A \ (Fr A) by ;
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 ;
set r2 = r / 2;
consider U being open Subset of (() | A) such that
A14: p in U and
A15: U c= Ball (p,(r / 2)) and
A16: for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) by ;
reconsider Sph = Sphere (p,(r / 2)) as non empty Subset of () by ;
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 ;
A21: Sph = (cl_Ball (p,(r / 2))) \ (Ball (p,(r / 2))) by ;
then W: au in cl_Ball (p,(r / 2)) by ;
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 () by A12;
A23: Sph c= CL2 by ;
[#] (() | CL2) = CL2 by PRE_TOPC:def 5;
then reconsider sph = Sph as non empty Subset of (() | CL2) by ;
A24: ((TOP-REAL n) | CL2) | sph = () | Sph by ;
not au in U by ;
then reconsider AU = A \ U as non empty Subset of () by ;
set TAU = () | AU;
set t = transl ((- p),());
set T = (transl ((- p),())) | (() | AU);
A25: [#] (() | AU) = A \ U by PRE_TOPC:def 5;
then A26: dom ((transl ((- p),())) | (() | AU)) = A \ U by FUNCT_2:def 1;
A27: (transl ((- p),())) | (() | AU) = (transl ((- p),())) | the carrier of (() | AU) by TMAP_1:def 4;
A28: rng ((transl ((- p),())) | (() | AU)) c= cTR0
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((transl ((- p),())) | (() | AU)) or y in cTR0 )
assume y in rng ((transl ((- p),())) | (() | AU)) ; :: thesis: y in cTR0
then consider x being object such that
A29: x in dom ((transl ((- p),())) | (() | AU)) and
A30: ((transl ((- p),())) | (() | AU)) . x = y by FUNCT_1:def 3;
reconsider x = x as Point of () by ;
A31: ((transl ((- p),())) | (() | AU)) . x = (transl ((- p),())) . x by ;
A32: (transl ((- p),())) . x = x + (- p) by RLTOPSP1:def 10;
assume not y in cTR0 ; :: thesis: contradiction
then ((transl ((- p),())) | (() | AU)) . x in {(0. ())} by ;
then x - p = 0. () by ;
then x = p by RLVECT_1:21;
hence contradiction by A29, A25, XBOOLE_0:def 5, A14; :: thesis: verum
end;
then reconsider T0 = (transl ((- p),())) | (() | AU) as continuous Function of (() | AU),(() | cTR0) by ;
A33: [#] (() | Sph) = Sph by PRE_TOPC:def 5;
A34: CL2 c= IA by ;
A35: CL2 c= A by A2, A20, A19, A13;
A36: dom b = cTR0 by ;
A37: for p being Point of () st p in cTR0 holds
( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )
proof
let p be Point of (); :: 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 ;
A41: nN0 . p = () . p by ;
thus b . p = (I . p) (/) (nN0 . p) by
.= p (/) |.p.| by
.= (1 / |.p.|) * p by VALUED_2:def 32 ; :: thesis: |.((1 / |.p.|) * p).| = 1
A42: p <> 0. () by ;
thus |.((1 / |.p.|) * p).| = |.(1 / |.p.|).| * |.p.| by TOPRNS_1:7
.= 1 by ; :: thesis: verum
end;
rng b c= Sphere ((0. ()),1)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng b or y in Sphere ((0. ()),1) )
assume y in rng b ; :: thesis: y in Sphere ((0. ()),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 () by ;
A45: |.((1 / |.x.|) * x).| = 1 by A3, A37, A43;
A46: ((1 / |.x.|) * x) - (0. ()) = (1 / |.x.|) * x by RLVECT_1:13;
y = (1 / |.x.|) * x by A3, A37, A43, A44;
hence y in Sphere ((0. ()),1) by ; :: thesis: verum
end;
then reconsider B = b as Function of (() | cTR0),() by ;
A47: [#] ((() | CL2) | sph) = sph by PRE_TOPC:def 5;
set m = mlt (r2,());
set M = (mlt (r2,())) | ();
reconsider M = (mlt (r2,())) | () as continuous Function of (),() by A1;
A48: M = (mlt (r2,())) | the carrier of () by TMAP_1:def 4;
A49: [#] (() | A) = A by PRE_TOPC:def 5;
then reconsider clB = CL2 as Subset of (() | A) by ;
A50: ((TOP-REAL n) | A) | clB = () | CL2 by ;
B is continuous by PRE_TOPC:27;
then B * T0 is continuous by TOPS_2:46;
then consider h being Function of (() | A),() such that
A51: h is continuous and
A52: h | (A \ U) = B * T0 by A16;
M * h is continuous Function of (() | A),() by ;
then reconsider GHM = (transl (p,())) * (M * h) as continuous Function of (() | A),() by TOPS_2:46;
A53: dom h = the carrier of (() | A) by ;
A54: |.r2.| = r2 by ;
A55: rng GHM c= Sph
proof
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,())) . ((M * h) . q) by ;
A59: q in A by ;
A60: q in dom (M * h) by ;
then A61: q in dom h by FUNCT_1:11;
A62: (M * h) . q = M . (h . q) by ;
A63: h . q in dom M by ;
reconsider q = q as Point of () by A59;
h . q in Sphere ((0. ()),1) by ;
then reconsider hq = h . q as Point of () ;
A64: (mlt (r2,())) . (h . q) = r2 * hq by RLTOPSP1:def 13;
M . (h . q) = (mlt (r2,())) . (h . q) by ;
then A65: y = p + (r2 * hq) by ;
A66: (p + (r2 * hq)) - p = (r2 * hq) + (p - p) by RLVECT_1:28
.= (r2 * hq) + (0. ()) by RLVECT_1:15
.= r2 * hq by RLVECT_1:def 4 ;
A67: h . q in rng h by ;
|.(r2 * hq).| = |.r2.| * |.hq.| by EUCLID:11
.= |.r2.| * 1 by ;
hence y in Sph by ; :: thesis: verum
end;
dom GHM = A by ;
then reconsider ghm = GHM as Function of (() | A),(() | Sph) by ;
ghm is continuous by PRE_TOPC:27;
then reconsider ghM = ghm | ((() | A) | clB) as continuous Function of (() | CL2),((() | CL2) | sph) by A8, A50, A24;
A68: dom ghM = the carrier of (() | CL2) by FUNCT_2:def 1;
A69: ghM = ghm | the carrier of ((() | A) | clB) by ;
for w being Point of (() | CL2) st w in Sph holds
ghM . w = w
proof
let w be Point of (() | 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 () ;
A71: w in CL2 by ;
w in A by ;
then A72: q in dom GHM by ;
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 ;
then A75: q in A \ U by ;
then q in (A \ U) /\ (dom h) by ;
then A76: q in dom (B * T0) by ;
then A77: (B * T0) . q = B . (T0 . q) by FUNCT_1:12;
A78: h . q in dom M by ;
then A79: M . (h . q) = (mlt (r2,())) . (h . q) by ;
(transl ((- p),())) . q = q + (- p) by RLTOPSP1:def 10;
then A80: ((transl ((- p),())) | (() | AU)) . q = q - p by ;
q in dom T0 by ;
then A81: ((transl ((- p),())) | (() | AU)) . q in rng ((transl ((- p),())) | (() | AU)) by FUNCT_1:def 3;
h . q in Sphere ((0. ()),1) by ;
then reconsider hq = h . q as Point of () ;
ghM . q = ghm . q by ;
then A82: ghM . q = (transl (p,())) . ((M * h) . q) by ;
hq = (B * T0) . q by ;
then A83: hq = (1 / |.(q - p).|) * (q - p) by A80, A77, A37, A81, A28;
(mlt (r2,())) . (h . q) = r2 * hq by RLTOPSP1:def 13
.= r2 * ((1 / r2) * (q - p)) by
.= (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
.= q + ((- p) + p) by RLVECT_1:def 3
.= q + (0. ()) by RLVECT_1:def 10
.= q by RLVECT_1:4 ;
hence ghM . w = w ; :: thesis: verum
end;
then A84: ghM is being_a_retraction by ;
Ball (p,r2) c= Int CL2 by ;
then A85: not CL2 is boundary by A12;
Fr CL2 = Sph by ;
hence contradiction by A84, A85, A47, BROUWER2:9, BORSUK_1:def 17; :: thesis: verum