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 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:11;
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;
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 object such that
A20: x in dom ((n NormF) | ((TOP-REAL n) | cTR0)) and
A21: ((n NormF) | ((TOP-REAL n) | cTR0)) . x = 0 by FUNCT_1:def 3;
x in dom (n NormF) by A19, A20, 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, A20, A21, 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, A20, 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;
A22: dom b = cTR0 by A10, FUNCT_2:def 1;
A23: 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 A24: p in cTR0 ; :: thesis:
then A25: ( 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 A22, A24, VALUED_2:72
.= p (/) |.p.| by A25, JGRAPH_4:def 1
.= (1 / |.p.|) (#) p by VALUED_2:def 32
.= (1 / |.p.|) * p ; :: thesis:
A26: ( |.(1 / |.p.|).| = 1 / |.p.| & p <> 0. (TOP-REAL n) ) by A24, ABSVALUE:def 1, ZFMISC_1:56;
thus |.((1 / |.p.|) * p).| = |.(1 / |.p.|).| * |.p.| by TOPRNS_1:7
.= 1 by A26, TOPRNS_1:24, XCMPLX_1:87 ; :: thesis:

end;

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng b ; :: thesis:
then consider x being object such that
A28: x in dom b and
A29: b . x = y by FUNCT_1:def 3;
reconsider x = x as Point of (TOP-REAL n) by A22, A28;
A30: ( ((1 / |.x.|) * x) - (0. (TOP-REAL n)) = (1 / |.x.|) * x & |.((1 / |.x.|) * x).| = 1 ) by A10, A23, A28;
y = (1 / |.x.|) * x by A10, A23, A28, A29;
hence y in Sphere ((0. (TOP-REAL n)),1) by A30; :: 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, A22, FUNCT_2:2;
A31: (0. (TOP-REAL n)) .--> (0. (TOP-REAL n)) = {(0. (TOP-REAL n))} --> (0. (TOP-REAL n)) by FUNCOP_1:def 9;
then A32: dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} ;
set FRA = ((TOP-REAL n) | cTR0) | FrA;
set H = b | (((TOP-REAL n) | cTR0) | FrA);
A33: dom (b | (((TOP-REAL n) | cTR0) | FrA)) = the carrier of (((TOP-REAL n) | cTR0) | FrA) by FUNCT_2:def 1;
A34: b | (((TOP-REAL n) | cTR0) | FrA) = b | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def 4;
then A35: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= rng b by RELAT_1:70;
then A36: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= Sphere ((0. (TOP-REAL n)),1) by A27;
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, A27, A33, A35, FUNCT_2:2, XBOOLE_1:1;
A37: [#] (((TOP-REAL n) | cTR0) | FrA) = FrA by PRE_TOPC:def 5;
A38: (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 object ; :: 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
A39: x = p and
A40: |.(p - (0. (TOP-REAL n))).| = 1 ;
p <> 0. (TOP-REAL n) by A5, A40;
then consider q being Point of (TOP-REAL n) such that
A41: FrA /\ (halfline ((0. (TOP-REAL n)),p)) = {q} by A13;
A42: q in {q} by TARSKI:def 1;
then A43: q in FrA by A41, XBOOLE_0:def 4;
then A44: ( b . q = (1 / |.q.|) * q & b . q = H . q ) by A9, A23, A34, A37, A38, FUNCT_1:49;
q in halfline ((0. (TOP-REAL n)),p) by A41, A42, XBOOLE_0:def 4;
then halfline ((0. (TOP-REAL n)),p) = halfline ((0. (TOP-REAL n)),q) by A5, A8, A43, TOPREAL9:31;
then A45: (1 / |.q.|) * q in halfline ((0. (TOP-REAL n)),p) by Lm2;
A46: ( ((1 / |.q.|) * q) - (0. (TOP-REAL n)) = (1 / |.q.|) * q & p in halfline ((0. (TOP-REAL n)),p) ) by TOPREAL9:28;
( H . q in rng H & |.((1 / |.q.|) * q).| = 1 ) by A9, A23, A33, A37, A38, A43, FUNCT_1:def 3;
hence x in rng H by A39, A40, A45, A46, A44, Th2; :: thesis:

end;

then A47: Sphere ((0. (TOP-REAL n)),1) = rng H by A36, XBOOLE_0:def 10;
(Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33;
then A48: ( 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 object 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 A68: p in cTR0 ; :: thesis:
then A69: p in dom NH1B by A10, FUNCT_2:def 1;
then A70: 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 A66;
A71: (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . Hp = nN0 . Hp by A63, A70, FUNCT_1:49;
A72: ( (n NormF) . Hp = |.Hp.| & nN0 . Hp = (n NormF) . Hp ) by A19, A66, A70, FUNCT_1:49, JGRAPH_4:def 1;
take Hp ; :: thesis:
thus ( Hp = H1B . p & Hp in FrA ) by A37, A70; :: thesis:
A73: NH1B . p = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . (H1B . p) by A69, FUNCT_1:12;
thus G . p = (I . p) (/) (NH1B . p) by A65, A68, VALUED_2:72
.= p (/) |.Hp.| by A10, A68, A73, A71, A72, TMAP_1:84
.= (1 / |.Hp.|) (#) p by VALUED_2:def 32
.= (1 / |.Hp.|) * p ; :: thesis:
|.Hp.| <> 0 by A63, A70, A73, A72, FUNCT_1:49;
hence |.Hp.| > 0 ; :: thesis:

end;

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

proof

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

end;

A78: 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
A79: x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) and
A80: x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) ; :: thesis:
x1 = 0. (TOP-REAL n) by A79, TARSKI:def 1;
then A81: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 = 0. (TOP-REAL n) by FUNCOP_1:72;
x2 in dom G by A80, XBOOLE_0:def 5;
hence ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 by A74, A81, FUNCT_1:def 3; :: thesis:

end;

H is onto by A18, A47, FUNCT_2:def 3;
then A82: H " = HH " by A62, TOPS_2:def 4;
A83: 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 A84: p in cTR0 ; :: thesis:
then A85: p in dom H1B by A10, FUNCT_2:def 1;
then A86: H1B . p = H1 . (B . p) by FUNCT_1:12;
B . p in dom H1 by A85, FUNCT_1:11;
then consider x being object such that
A87: x in dom H and
A88: H . x = B . p by A18, A47, FUNCT_1:def 3;
reconsider x = x as Point of (TOP-REAL n) by A33, A37, A87;
A89: H . x = b . x by A34, A87, FUNCT_1:47;
set xp = |.x.| / |.p.|;
A90: x in FrA by A37, A87;
then A91: b . x = (1 / |.x.|) * x by A9, A23, A38;
|.((1 / |.x.|) * x).| = 1 by A9, A23, A38, A90;
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 A23, A84, A88, A89, A91
.= (|.x.| / |.p.|) * p by RLVECT_1:def 7 ;
then x in halfline ((0. (TOP-REAL n)),p) by Lm2;
then A92: x in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A37, A87, XBOOLE_0:def 4;
p <> 0. (TOP-REAL n) by A84, ZFMISC_1:56;
then consider y being Point of (TOP-REAL n) such that
A93: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {y} by A13;
H1 . (B . p) = x by A62, A82, A87, A88, FUNCT_1:34;
hence (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} by A86, A92, A93, TARSKI:def 1; :: thesis:

end;

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

proof

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

end;

then A104: G is one-to-one by FUNCT_1:def 4;
set G0 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)));
A105: 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 A31, A65
.= the carrier of (TOP-REAL n) by ZFMISC_1:116 ;
A106: 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
A107: p in cTR0 and
A108: Hp1 = H1B . p ; :: thesis:
reconsider p = p as Point of (TOP-REAL n) ;
consider Hp being Point of (TOP-REAL n) such that
A109: Hp = H1B . p and
Hp in FrA and
G . p = (1 / |.Hp.|) * p and
A110: |.Hp.| > 0 by A67, A107;
set Hpp = |.Hp.| * p;
p <> 0. (TOP-REAL n) by A107, ZFMISC_1:56;
then A111: |.Hp.| * p <> 0. (TOP-REAL n) by A110, RLVECT_1:11;
then A112: |.Hp.| * p in cTR0 by ZFMISC_1:56;
then consider HP being Point of (TOP-REAL n) such that
A113: HP = H1B . (|.Hp.| * p) and
HP in FrA and
A114: G . (|.Hp.| * p) = (1 / |.HP.|) * (|.Hp.| * p) and
|.HP.| > 0 by A67;
A115: Hp in {Hp} by TARSKI:def 1;
{HP} = (Fr A) /\ (halfline ((0. (TOP-REAL n)),(|.Hp.| * p))) by A83, A112, A113
.= (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A111, Lm2, TOPREAL9:31
.= {Hp} by A83, A107, A109 ;
then G . (|.Hp.| * p) = (1 / |.Hp.|) * (|.Hp.| * p) by A114, A115, TARSKI:def 1
.= (|.Hp.| / |.Hp.|) * p by RLVECT_1:def 7
.= 1 * p by A110, XCMPLX_1:60
.= p by RLVECT_1:def 8 ;
hence ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) by A65, A108, A109, A111, ZFMISC_1:56; :: thesis:

end;

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

proof

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

end;

A125: 0. (TOP-REAL n) in {(0. (TOP-REAL n))} by TARSKI:def 1;
then A126: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) = 0. (TOP-REAL n) by A31, FUNCOP_1:7;
rng ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by A31, FUNCOP_1:8;
then rng (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (rng G) \/ {(0. (TOP-REAL n))} by A32, A65, 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 A105, A78, A104, FUNCT_2:2, TOPMETR2:1;
A127: G1 . (0. (TOP-REAL n)) = ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) by A32, A125, FUNCT_4:13;
A128: G .: FrA c= Sphere ((0. (TOP-REAL n)),1)

proof

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

end;

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A143: 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, A137, A5, A126, A138, A139, A127, FUNCT_1:49;
hence p in rng (G1 | ((TOP-REAL n) | A)) by A3, A137, A5, A139, A141, FUNCT_1:def 3; :: thesis:

end;

suppose A144: 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 object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (G1 | ((TOP-REAL n) | A)) ; :: thesis:
then consider p being object such that
A156: p in dom (G1 | ((TOP-REAL n) | A)) and
A157: (G1 | ((TOP-REAL n) | A)) . p = x by FUNCT_1:def 3;
reconsider p = p as Point of (TOP-REAL n) by A140, A156;
A158: (G1 | ((TOP-REAL n) | A)) . p = G1 . p by A138, A156, FUNCT_1:47;
A159: (G1 . p) - (0. (TOP-REAL n)) = G1 . p ;

per cases ;

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

then G1 . p = 0. (TOP-REAL n) by A31, A125, A127, FUNCOP_1:7;
then |.((G1 . p) - (0. (TOP-REAL n))).| = 0 by TOPRNS_1:23;
hence x in cl_Ball ((0. (TOP-REAL n)),1) by A157, A158; :: thesis:

end;

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

end;

then A171: rng (G1 | ((TOP-REAL n) | A)) = cl_Ball ((0. (TOP-REAL n)),1) by A142, XBOOLE_0:def 10;
A172: [#] ((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 A139, A140, A171, FUNCT_2:1;
set e2 = e / 2;
A173: GA is one-to-one by A138, FUNCT_1:52;
A174: e / 2 < e by A6, XREAL_1:216;
A175: 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 A176: x <> 0. (TOP-REAL n) ; :: thesis:

then A177: x in dom G by A65, 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 A176, TARSKI:def 1;
then A178: G . x = G1 . x by FUNCT_4:11;
then A179: G1 . x <> 0. (TOP-REAL n) by A74, A177, 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 A179, 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
A180: G .: H c= cTR0 /\ U by A178, 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 A31, BOOLMARK:3, XBOOLE_1:17;
hence ex b₁ being a_neighborhood of x st G1 .: b₁ c= U by A180, XBOOLE_1:1; :: thesis:
reconsider U1 = cTR0 /\ U as Subset of ((TOP-REAL n) | cTR0) by A10, XBOOLE_1:17;

end;

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

reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
A182: 0. (TOP-REAL n) in Int U by A126, A127, A181, CONNSP_2:def 1;
then consider r being Real such that
A183: r > 0 and
A184: 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, A183, GOBOARD6:5;
then reconsider Bx = B as a_neighborhood of x by A181, CONNSP_2:def 1;
take Bx ; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A185: y in G1 .: Bx ; :: thesis:
then reconsider p = y as Point of (TOP-REAL n) ;
A186: Int U c= U by TOPS_1:16;

per cases ;

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

hence y in U by A182, A186; :: thesis:

end;

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

end;

GA .: FrA = G1 .: FrA by A2, A138, A139, RELAT_1:129, TOPS_1:35;
then GA .: FrA = G .: FrA by A5, A8, A31, BOOLMARK:3, ZFMISC_1:50;
then A204: GA .: FrA = Sphere ((0. (TOP-REAL n)),1) by A116, A128, XBOOLE_0:def 10;
( dom GA = [#] ((TOP-REAL n) | A) & rng GA = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) ) by A142, A172, FUNCT_2:def 1, XBOOLE_0:def 10;
then GA is being_homeomorphism by A2, A3, A137, A173, A175, 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 A204; :: thesis: