let n be Element of NAT ; :: thesis:
set TRn = TOP-REAL n;
set En = Euclid n;
set cTRn = the carrier of (TOP-REAL n);
assume A1: n > 0 ; :: thesis:
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 CL = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
set TRn0 = (TOP-REAL n) | cTR0;
set nN = n NormF ;
set En = Euclid n;
set I0 = (0. (TOP-REAL n)) .--> (0. (TOP-REAL n));
let A be convex Subset of (TOP-REAL n); :: thesis:
assume that
A2: A is compact and
A3: 0* n in Int A ; :: thesis:
A4: not A is empty by A3;
reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
A5: 0* n = 0. (TOP-REAL n) by EUCLID:70;
then consider e being real number such that
A6: e > 0 and
A7: Ball (0TRn,e) c= A by A3, GOBOARD6:5;
Fr A misses Int A by TOPS_1:39;
then A8: not 0* n in Fr A by A3, XBOOLE_0:3;
then A9: (Fr A) \ {(0. (TOP-REAL n))} = Fr A by A5, ZFMISC_1:57;
set TM = TopSpaceMetr (Euclid n);
A10: [#] ((TOP-REAL n) | cTR0) = cTR0 by PRE_TOPC:def 5;
A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider a = A as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider aa = a as Subset of (Euclid n) by EUCLID:67;
(TOP-REAL n) | A is compact by A2;
then (TopSpaceMetr (Euclid n)) | a is compact by A11, PRE_TOPC:36;
then A12: a is compact by A4, COMPTS_1:3;
A13: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x}

proof

let p be Point of (TOP-REAL n); :: thesis:
assume A14: p <> 0. (TOP-REAL n) ; :: thesis:
A15: A /\ (halfline ((0. (TOP-REAL n)),p)) c= aa by XBOOLE_1:17;
then reconsider F = A /\ (halfline ((0. (TOP-REAL n)),p)) as Subset of (Euclid n) by XBOOLE_1:1;
A16: 0. (TOP-REAL n) in Int A by A3, EUCLID:70;
F is bounded by A12, A15, HAUSDORF:18, TBSP_1:14;
then A /\ (halfline ((0. (TOP-REAL n)),p)) is Bounded by JORDAN2C:def 1;
hence ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} by A2, A14, A16, Th4; :: thesis:

end;

not Fr A is empty

proof

set q = the Element of cTR0;
the Element of cTR0 <> 0. (TOP-REAL n) by ZFMISC_1:56;
then ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)), the Element of cTR0)) = {x} by A13;
hence not Fr A is empty ; :: thesis:

end;

then reconsider FrA = Fr A as non empty Subset of ((TOP-REAL n) | cTR0) by A10, A9, XBOOLE_1:33;
A17: Fr A c= A by A2, TOPS_1:35;
set TS = (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1));
reconsider I = incl ((TOP-REAL n) | cTR0) as continuous Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TMAP_1:87;
A18: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
A19: (n NormF) | ((TOP-REAL n) | cTR0) = (n NormF) | the carrier of ((TOP-REAL n) | cTR0) by TMAP_1:def 4;
A20: not 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0))

proof

assume 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0)) ; :: thesis:
then consider x being set such that
A21: x in dom ((n NormF) | ((TOP-REAL n) | cTR0)) and
A22: ((n NormF) | ((TOP-REAL n) | cTR0)) . x = 0 by FUNCT_1:def 3;
x in dom (n NormF) by A19, A21, 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 A19, A21, A22, FUNCT_1:47
.= |.X.| by JGRAPH_4:def 1 ;
then x = 0. (TOP-REAL n) by A5, EUCLID:8;
then x in {(0. (TOP-REAL n))} by TARSKI:def 1;
hence contradiction by A10, A21, XBOOLE_0:def 5; :: thesis:

end;

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;
reconsider b = I </> nN0 as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;
A23: dom b = cTR0 by A10, FUNCT_2:def 1;
A24: for p being Point of (TOP-REAL n) st p in cTR0 holds
( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )

proof

let p be Point of (TOP-REAL n); :: thesis:
assume A25: p in cTR0 ; :: thesis:
then A26: ( nN0 . p = (n NormF) . p & I . p = p ) by A10, A19, FUNCT_1:49, TMAP_1:84;
thus b . p = (I . p) (/) (nN0 . p) by A23, A25, VALUED_2:72
.= p (/) |.p.| by A26, JGRAPH_4:def 1
.= (1 / |.p.|) (#) p by VALUED_2:def 32
.= (1 / |.p.|) * p ; :: thesis:
A27: ( abs (1 / |.p.|) = 1 / |.p.| & p <> 0. (TOP-REAL n) ) by A25, ABSVALUE:def 1, ZFMISC_1:56;
thus |.((1 / |.p.|) * p).| = (abs (1 / |.p.|)) * |.p.| by TOPRNS_1:7
.= 1 by A27, TOPRNS_1:24, XCMPLX_1:87 ; :: thesis:

end;

A28: rng b c= Sphere ((0. (TOP-REAL n)),1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng b ; :: thesis:
then consider x being set such that
A29: x in dom b and
A30: b . x = y by FUNCT_1:def 3;
reconsider x = x as Point of (TOP-REAL n) by A23, A29;
A31: ( ((1 / |.x.|) * x) - (0. (TOP-REAL n)) = (1 / |.x.|) * x & |.((1 / |.x.|) * x).| = 1 ) by A10, A24, A29, RLVECT_1:13;
y = (1 / |.x.|) * x by A10, A24, A29, A30;
hence y in Sphere ((0. (TOP-REAL n)),1) by A31; :: thesis:

end;

then reconsider B = b as Function of ((TOP-REAL n) | cTR0),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A10, A18, A23, FUNCT_2:2;
A32: (0. (TOP-REAL n)) .--> (0. (TOP-REAL n)) = {(0. (TOP-REAL n))} --> (0. (TOP-REAL n)) by FUNCOP_1:def 9;
then A33: dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by FUNCOP_1:13;
set FRA = ((TOP-REAL n) | cTR0) | FrA;
set H = b | (((TOP-REAL n) | cTR0) | FrA);
A34: dom (b | (((TOP-REAL n) | cTR0) | FrA)) = the carrier of (((TOP-REAL n) | cTR0) | FrA) by FUNCT_2:def 1;
A35: b | (((TOP-REAL n) | cTR0) | FrA) = b | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def 4;
then A36: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= rng b by RELAT_1:70;
then A37: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= Sphere ((0. (TOP-REAL n)),1) by A28, XBOOLE_1:1;
reconsider H = b | (((TOP-REAL n) | cTR0) | FrA) as Function of (((TOP-REAL n) | cTR0) | FrA),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A18, A28, A34, A36, FUNCT_2:2, XBOOLE_1:1;
A38: [#] (((TOP-REAL n) | cTR0) | FrA) = FrA by PRE_TOPC:def 5;
A39: (Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33;
Sphere ((0. (TOP-REAL n)),1) c= rng H

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Sphere ((0. (TOP-REAL n)),1) ; :: thesis:
then consider p being Point of (TOP-REAL n) such that
A40: x = p and
A41: |.(p - (0. (TOP-REAL n))).| = 1 ;
p <> 0. (TOP-REAL n) by A5, A41;
then consider q being Point of (TOP-REAL n) such that
A42: FrA /\ (halfline ((0. (TOP-REAL n)),p)) = {q} by A13;
A43: q in {q} by TARSKI:def 1;
then A44: q in FrA by A42, XBOOLE_0:def 4;
then A45: ( b . q = (1 / |.q.|) * q & b . q = H . q ) by A9, A24, A35, A38, A39, FUNCT_1:49;
q in halfline ((0. (TOP-REAL n)),p) by A42, A43, XBOOLE_0:def 4;
then halfline ((0. (TOP-REAL n)),p) = halfline ((0. (TOP-REAL n)),q) by A5, A8, A44, TOPREAL9:31;
then A46: (1 / |.q.|) * q in halfline ((0. (TOP-REAL n)),p) by Lm2;
A47: ( ((1 / |.q.|) * q) - (0. (TOP-REAL n)) = (1 / |.q.|) * q & p in halfline ((0. (TOP-REAL n)),p) ) by RLVECT_1:13, TOPREAL9:28;
( H . q in rng H & |.((1 / |.q.|) * q).| = 1 ) by A9, A24, A34, A38, A39, A44, FUNCT_1:def 3;
hence x in rng H by A40, A41, A46, A47, A45, Th2; :: thesis:

end;

then A48: Sphere ((0. (TOP-REAL n)),1) = rng H by A37, XBOOLE_0:def 10;
(Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33;
then A49: ( dom H = [#] (((TOP-REAL n) | cTR0) | FrA) & (TOP-REAL n) | (Fr A) = ((TOP-REAL n) | cTR0) | FrA ) by A9, FUNCT_2:def 1, PRE_TOPC:7;
for x1, x2 being set st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds
x1 = x2

proof

end;

proof

let p be Point of (TOP-REAL n); :: thesis:
assume A69: p in cTR0 ; :: thesis:
then A70: p in dom NH1B by A10, FUNCT_2:def 1;
then A71: H1B . p in dom (nN0 | (((TOP-REAL n) | cTR0) | FrA)) by FUNCT_1:11;
then reconsider Hp = H1B . p as Point of (TOP-REAL n) by A67;
A72: (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . Hp = nN0 . Hp by A64, A71, FUNCT_1:49;
A73: ( (n NormF) . Hp = |.Hp.| & nN0 . Hp = (n NormF) . Hp ) by A19, A67, A71, FUNCT_1:49, JGRAPH_4:def 1;
take Hp ; :: thesis:
A74: NH1B . p = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . (H1B . p) by A70, FUNCT_1:12;
G . p = (I . p) (/) (NH1B . p) by A66, A69, VALUED_2:72
.= p (/) |.Hp.| by A10, A69, A74, A72, A73, TMAP_1:84
.= (1 / |.Hp.|) (#) p by VALUED_2:def 32
.= (1 / |.Hp.|) * p ;
hence ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) by A38, A64, A70, A71, A74, A73, FUNCT_1:49; :: thesis:

end;

A75: not 0. (TOP-REAL n) in rng G

proof

assume 0. (TOP-REAL n) in rng G ; :: thesis:
then consider p being set such that
A76: p in dom G and
A77: G . p = 0. (TOP-REAL n) by FUNCT_1:def 3;
reconsider p = p as Point of (TOP-REAL n) by A66, A76;
consider Hp being Point of (TOP-REAL n) such that
Hp = H1B . p and
Hp in FrA and
A78: ( G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) by A10, A68, A76;
p <> 0. (TOP-REAL n) by A10, A76, ZFMISC_1:56;
hence contradiction by A77, A78, RLVECT_1:11; :: thesis:

end;

A79: for x1, x2 being set st x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) & x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) holds
((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2

proof

let x1, x2 be set ; :: thesis:
assume that
A80: x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) and
A81: x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) ; :: thesis:
x1 = 0. (TOP-REAL n) by A33, A80, TARSKI:def 1;
then A82: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 = 0. (TOP-REAL n) by FUNCOP_1:72;
x2 in dom G by A81, XBOOLE_0:def 5;
hence ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 by A75, A82, FUNCT_1:def 3; :: thesis:

end;

H is onto by A18, A48, FUNCT_2:def 3;
then A84: H " = HH " by CC, TOPS_2:def 4;
A85: for p being Point of (TOP-REAL n) st p in cTR0 holds
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)}

proof

let p be Point of (TOP-REAL n); :: thesis:
assume A86: p in cTR0 ; :: thesis:
then A87: p in dom H1B by A10, FUNCT_2:def 1;
then A88: H1B . p = H1 . (B . p) by FUNCT_1:12;
B . p in dom H1 by A87, FUNCT_1:11;
then consider x being set such that
A89: x in dom H and
A90: H . x = B . p by A18, A48, FUNCT_1:def 3;
reconsider x = x as Point of (TOP-REAL n) by A34, A38, A89;
A91: H . x = b . x by A35, A89, FUNCT_1:47;
set xp = |.x.| / |.p.|;
A92: x in FrA by A38, A89;
then A93: b . x = (1 / |.x.|) * x by A9, A24, A39;
|.((1 / |.x.|) * x).| = 1 by A9, A24, A39, A92;
then (1 / |.x.|) * x <> 0. (TOP-REAL n) by TOPRNS_1:23;
then 1 / |.x.| <> 0 by RLVECT_1:10;
then |.x.| > 0 ;
then 1 = |.x.| / |.x.| by XCMPLX_1:60
.= |.x.| * (1 / |.x.|) ;
then x = (|.x.| * (1 / |.x.|)) * x by RLVECT_1:def 8
.= |.x.| * ((1 / |.x.|) * x) by RLVECT_1:def 7
.= |.x.| * ((1 / |.p.|) * p) by A24, A86, A90, A91, A93
.= (|.x.| / |.p.|) * p by RLVECT_1:def 7 ;
then x in halfline ((0. (TOP-REAL n)),p) by Lm2;
then A94: x in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A38, A89, XBOOLE_0:def 4;
p <> 0. (TOP-REAL n) by A86, ZFMISC_1:56;
then consider y being Point of (TOP-REAL n) such that
A95: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {y} by A13;
H1 . (B . p) = x by CC, A84, A89, A90, FUNCT_1:34;
hence (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} by A88, A94, A95, TARSKI:def 1; :: thesis:

end;

for x1, x2 being set st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume that
A96: x1 in dom G and
A97: x2 in dom G and
A98: G . x1 = G . x2 ; :: thesis:
reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL n) by A66, A96, A97;
consider Hp1 being Point of (TOP-REAL n) such that
A99: Hp1 = H1B . p1 and
Hp1 in FrA and
A100: G . p1 = (1 / |.Hp1.|) * p1 and
A101: |.Hp1.| > 0 by A10, A68, A96;
A102: FrA /\ (halfline ((0. (TOP-REAL n)),p1)) = {Hp1} by A10, A85, A96, A99;
consider Hp2 being Point of (TOP-REAL n) such that
A103: Hp2 = H1B . p2 and
Hp2 in FrA and
A104: G . p2 = (1 / |.Hp2.|) * p2 and
|.Hp2.| > 0 by A10, A68, A97;
p1 <> 0. (TOP-REAL n) by A10, A96, ZFMISC_1:56;
then A105: (1 / |.Hp1.|) * p1 <> 0. (TOP-REAL n) by A101, RLVECT_1:11;
then halfline ((0. (TOP-REAL n)),p1) = halfline ((0. (TOP-REAL n)),((1 / |.Hp1.|) * p1)) by Lm2, TOPREAL9:31
.= halfline ((0. (TOP-REAL n)),p2) by A98, A100, A104, A105, Lm2, TOPREAL9:31 ;
then ( Hp1 in {Hp1} & {Hp1} = {Hp2} ) by A10, A85, A97, A102, A103, TARSKI:def 1;
then 1 / |.Hp1.| = 1 / |.Hp2.| by TARSKI:def 1;
hence x1 = x2 by A98, A100, A101, A104, RLVECT_1:36; :: thesis:

end;

then A106: G is one-to-one by FUNCT_1:def 4;
set G0 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)));
A107: dom (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (dom G) \/ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) by FUNCT_4:def 1
.= cTR0 \/ {(0. (TOP-REAL n))} by A32, A66, FUNCOP_1:13
.= the carrier of (TOP-REAL n) by ZFMISC_1:116 ;
A108: for p, Hp being Point of (TOP-REAL n) st p in cTR0 & Hp = H1B . p holds
( p = G . (|.Hp.| * p) & |.Hp.| * p in dom G )

proof

let p, Hp1 be Point of (TOP-REAL n); :: thesis:
assume that
A109: p in cTR0 and
A110: Hp1 = H1B . p ; :: thesis:
reconsider p = p as Point of (TOP-REAL n) ;
consider Hp being Point of (TOP-REAL n) such that
A111: Hp = H1B . p and
Hp in FrA and
G . p = (1 / |.Hp.|) * p and
A112: |.Hp.| > 0 by A68, A109;
set Hpp = |.Hp.| * p;
p <> 0. (TOP-REAL n) by A109, ZFMISC_1:56;
then A113: |.Hp.| * p <> 0. (TOP-REAL n) by A112, RLVECT_1:11;
then A114: |.Hp.| * p in cTR0 by ZFMISC_1:56;
then consider HP being Point of (TOP-REAL n) such that
A115: HP = H1B . (|.Hp.| * p) and
HP in FrA and
A116: G . (|.Hp.| * p) = (1 / |.HP.|) * (|.Hp.| * p) and
|.HP.| > 0 by A68;
A117: Hp in {Hp} by TARSKI:def 1;
{HP} = (Fr A) /\ (halfline ((0. (TOP-REAL n)),(|.Hp.| * p))) by A85, A114, A115
.= (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A113, Lm2, TOPREAL9:31
.= {Hp} by A85, A109, A111 ;
then G . (|.Hp.| * p) = (1 / |.Hp.|) * (|.Hp.| * p) by A116, A117, TARSKI:def 1
.= (|.Hp.| / |.Hp.|) * p by RLVECT_1:def 7
.= 1 * p by A112, XCMPLX_1:60
.= p by RLVECT_1:def 8 ;
hence ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) by A66, A110, A111, A113, ZFMISC_1:56; :: thesis:

end;

A118: Sphere ((0. (TOP-REAL n)),1) c= G .: FrA

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A119: p in Sphere ((0. (TOP-REAL n)),1) ; :: thesis:
then reconsider p = p as Point of (TOP-REAL n) ;
|.p.| = 1 by A119, TOPREAL9:12;
then p <> 0. (TOP-REAL n) by TOPRNS_1:23;
then A120: p in cTR0 by ZFMISC_1:56;
then consider Hp being Point of (TOP-REAL n) such that
A121: Hp = H1B . p and
A122: Hp in FrA and
G . p = (1 / |.Hp.|) * p and
|.Hp.| > 0 by A68;
set Hpp = |.Hp.| * p;
A123: ( p = G . (|.Hp.| * p) & |.Hp.| * p in dom G ) by A108, A120, A121;
( Hp in {Hp} & (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} ) by A85, A120, A121, TARSKI:def 1;
then A124: Hp in halfline ((0. (TOP-REAL n)),p) by XBOOLE_0:def 4;
A125: Hp - (0. (TOP-REAL n)) = Hp by RLVECT_1:13;
abs |.Hp.| = |.Hp.| by ABSVALUE:def 1;
then A126: |.(|.Hp.| * p).| = |.Hp.| * |.p.| by TOPRNS_1:7
.= |.Hp.| * 1 by A119, TOPREAL9:12 ;
( (|.Hp.| * p) - (0. (TOP-REAL n)) = |.Hp.| * p & |.Hp.| * p in halfline ((0. (TOP-REAL n)),p) ) by Lm2, RLVECT_1:13;
then Hp = |.Hp.| * p by A126, A124, A125, Th2;
hence p in G .: FrA by A122, A123, FUNCT_1:def 6; :: thesis:

end;

A127: 0. (TOP-REAL n) in {(0. (TOP-REAL n))} by TARSKI:def 1;
then A128: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) = 0. (TOP-REAL n) by A32, FUNCOP_1:7;
rng ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by A32, FUNCOP_1:8;
then rng (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (rng G) \/ {(0. (TOP-REAL n))} by A33, A66, NECKLACE:6, XBOOLE_1:79;
then reconsider G1 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) as one-to-one Function of (TOP-REAL n),(TOP-REAL n) by A107, A79, A106, FUNCT_2:2, TOPMETR2:1;
A129: G1 . (0. (TOP-REAL n)) = ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) by A33, A127, FUNCT_4:13;
A130: G .: FrA c= Sphere ((0. (TOP-REAL n)),1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in G .: FrA ; :: thesis:
then consider p being set such that
A131: p in dom G and
A132: p in FrA and
A133: G . p = y by FUNCT_1:def 6;
reconsider p = p as Point of (TOP-REAL n) by A132;
consider Hp being Point of (TOP-REAL n) such that
A134: Hp = H1B . p and
Hp in FrA and
A135: G . p = (1 / |.Hp.|) * p and
A136: |.Hp.| > 0 by A10, A68, A131;
p in halfline ((0. (TOP-REAL n)),p) by TOPREAL9:28;
then A137: p in FrA /\ (halfline ((0. (TOP-REAL n)),p)) by A132, XBOOLE_0:def 4;
FrA /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A10, A85, A131, A134;
then A138: p = Hp by A137, TARSKI:def 1;
abs (1 / |.Hp.|) = 1 / |.Hp.| by ABSVALUE:def 1;
then |.((1 / |.Hp.|) * p).| = (1 / |.Hp.|) * |.Hp.| by A138, TOPRNS_1:7
.= 1 by A136, XCMPLX_1:106 ;
then |.(((1 / |.Hp.|) * p) - (0. (TOP-REAL n))).| = 1 by RLVECT_1:13;
hence y in Sphere ((0. (TOP-REAL n)),1) by A133, A135; :: thesis:

end;

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A145: p in cl_Ball ((0. (TOP-REAL n)),1) ; :: thesis:
then reconsider p = p as Point of (TOP-REAL n) ;

per cases ;

suppose p = 0. (TOP-REAL n) ; :: thesis:

then p = (G1 | ((TOP-REAL n) | A)) . (0. (TOP-REAL n)) by A3, A139, A5, A128, A140, A141, A129, FUNCT_1:49;
hence p in rng (G1 | ((TOP-REAL n) | A)) by A3, A139, A5, A141, A143, FUNCT_1:def 3; :: thesis:

end;

suppose A146: p <> 0. (TOP-REAL n) ; :: thesis:

end;

rng (G1 | ((TOP-REAL n) | A)) c= cl_Ball ((0. (TOP-REAL n)),1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (G1 | ((TOP-REAL n) | A)) ; :: thesis:
then consider p being set such that
A158: p in dom (G1 | ((TOP-REAL n) | A)) and
A159: (G1 | ((TOP-REAL n) | A)) . p = x by FUNCT_1:def 3;
reconsider p = p as Point of (TOP-REAL n) by A142, A158;
A160: (G1 | ((TOP-REAL n) | A)) . p = G1 . p by A140, A158, FUNCT_1:47;
A161: (G1 . p) - (0. (TOP-REAL n)) = G1 . p by RLVECT_1:13;

per cases ;

suppose p = 0. (TOP-REAL n) ; :: thesis:

then G1 . p = 0. (TOP-REAL n) by A32, A127, A129, FUNCOP_1:7;
then |.((G1 . p) - (0. (TOP-REAL n))).| = 0 by A161, TOPRNS_1:23;
hence x in cl_Ball ((0. (TOP-REAL n)),1) by A159, A160; :: thesis:

end;

suppose A162: p <> 0. (TOP-REAL n) ; :: thesis:

end;

then A173: rng (G1 | ((TOP-REAL n) | A)) = cl_Ball ((0. (TOP-REAL n)),1) by A144, XBOOLE_0:def 10;
A174: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
then reconsider GA = G1 | ((TOP-REAL n) | A) as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A141, A142, A173, FUNCT_2:1;
set e2 = e / 2;
A175: GA is one-to-one by A140, FUNCT_1:52;
A176: e / 2 < e by A6, XREAL_1:216;
A177: G1 is continuous

proof

let x be Point of (TOP-REAL n); :: according to BORSUK_1:def 1 :: thesis:
let U be a_neighborhood of G1 . x; :: thesis:

per cases ;

suppose A178: x <> 0. (TOP-REAL n) ; :: thesis:

then A179: x in dom G by A66, ZFMISC_1:56;
then reconsider X = x as Point of ((TOP-REAL n) | cTR0) ;
not x in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by A33, A178, TARSKI:def 1;
then A180: G . x = G1 . x by FUNCT_4:11;
then A181: G1 . x <> 0. (TOP-REAL n) by A75, A179, FUNCT_1:def 3;
then reconsider G1x = G1 . x as Point of ((TOP-REAL n) | cTR0) by A10, ZFMISC_1:56;
G1 . x in cTR0 by A181, ZFMISC_1:56;
then cTR0 is a_neighborhood of G1 . x by CONNSP_2:3;
then cTR0 /\ U is a_neighborhood of G1 . x by CONNSP_2:2;
then consider H being a_neighborhood of X such that
A182: G .: H c= cTR0 /\ U by A180, BORSUK_1:def 1;
reconsider h = H as Subset of (TOP-REAL n) by A10, XBOOLE_1:1;
reconsider h = h as a_neighborhood of x by CONNSP_2:9;
{(0. (TOP-REAL n))} misses H by A10, XBOOLE_1:63, XBOOLE_1:79;
then ( cTR0 /\ U c= U & G .: H = G1 .: h ) by A32, BOOLMARK:3, XBOOLE_1:17;
hence ex b₁ being a_neighborhood of x st G1 .: b₁ c= U by A182, XBOOLE_1:1; :: thesis:
reconsider U1 = cTR0 /\ U as Subset of ((TOP-REAL n) | cTR0) by A10, XBOOLE_1:17;

end;

suppose A183: x = 0. (TOP-REAL n) ; :: thesis:

reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
A184: 0. (TOP-REAL n) in Int U by A128, A129, A183, CONNSP_2:def 1;
then consider r being real number such that
A185: r > 0 and
A186: Ball (0TRn,r) c= U by GOBOARD6:5;
reconsider B = Ball (0TRn,(r * (e / 2))) as Subset of (TOP-REAL n) by EUCLID:67;
0TRn in Int B by A6, A185, GOBOARD6:5;
then reconsider Bx = B as a_neighborhood of x by A183, CONNSP_2:def 1;
take Bx ; :: thesis:
let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A187: y in G1 .: Bx ; :: thesis:
then reconsider p = y as Point of (TOP-REAL n) ;
A188: Int U c= U by TOPS_1:16;

per cases ;

suppose y = 0. (TOP-REAL n) ; :: thesis:

hence y in U by A184, A188; :: thesis:

end;

suppose A189: p <> 0. (TOP-REAL n) ; :: thesis:

end;

GA .: FrA = G1 .: FrA by A2, A140, A141, RELAT_1:129, TOPS_1:35;
then GA .: FrA = G .: FrA by A5, A8, A32, BOOLMARK:3, ZFMISC_1:50;
then A206: GA .: FrA = Sphere ((0. (TOP-REAL n)),1) by A118, A130, XBOOLE_0:def 10;
( dom GA = [#] ((TOP-REAL n) | A) & rng GA = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) ) by A144, A174, FUNCT_2:def 1, XBOOLE_0:def 10;
then GA is being_homeomorphism by A2, A3, A139, A175, A177, COMPTS_1:17, PRE_TOPC:27;
hence 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) ) by A206; :: thesis: