let n be Element of NAT ; ( n > 0 implies for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds
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) ) )
set TRn = TOP-REAL n;
set En = Euclid n;
set cTRn = the carrier of (TOP-REAL n);
assume A1:
n > 0
; for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds
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) )
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); ( A is compact & 0* n in Int A implies 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) ) )
assume that
A2:
A is compact
and
A3:
0* n in Int A
; 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) )
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);
( p <> 0. (TOP-REAL n) implies ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} )
assume A14:
p <> 0. (TOP-REAL n)
;
ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x}
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;
verum
end;
not Fr A is empty
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))
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);
( p in cTR0 implies ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) )
assume A24:
p in cTR0
;
( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )
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
;
|.((1 / |.p.|) * p).| = 1
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
;
verum
end;
A27:
rng b c= Sphere ((0. (TOP-REAL n)),1)
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 ;
TARSKI:def 3 ( not x in Sphere ((0. (TOP-REAL n)),1) or x in rng H )
assume
x in Sphere (
(0. (TOP-REAL n)),1)
;
x in rng H
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;
verum
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
let x1,
x2 be
object ;
( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )
assume that A49:
x1 in dom H
and A50:
x2 in dom H
and A51:
H . x1 = H . x2
;
x1 = x2
A52:
x2 in dom b
by A34, A50, RELAT_1:57;
A53:
x1 in dom b
by A34, A49, RELAT_1:57;
then reconsider p1 =
x1,
p2 =
x2 as
Point of
(TOP-REAL n) by A22, A52;
A54:
b . p1 = (1 / |.p1.|) * p1
by A10, A23, A53;
x2 <> 0. (TOP-REAL n)
by A10, A52, ZFMISC_1:56;
then consider q being
Point of
(TOP-REAL n) such that A55:
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p2)) = {q}
by A13;
p2 in halfline (
(0. (TOP-REAL n)),
p2)
by TOPREAL9:28;
then
p2 in {q}
by A37, A50, A55, XBOOLE_0:def 4;
then A56:
p2 = q
by TARSKI:def 1;
|.((1 / |.p2.|) * p2).| = 1
by A10, A23, A52;
then A57:
(1 / |.p2.|) * p2 <> 0. (TOP-REAL n)
by TOPRNS_1:23;
A58:
(0. (TOP-REAL n)) + ((1 / |.p2.|) * p2) = (1 / |.p2.|) * p2
;
A59:
b . p2 = (1 / |.p2.|) * p2
by A10, A23, A52;
A60:
(
H . x1 = b . x1 &
H . x2 = b . x2 )
by A34, A49, A50, FUNCT_1:47;
(1 - (1 / |.p1.|)) * (0. (TOP-REAL n)) = 0. (TOP-REAL n)
;
then A61:
(1 / |.p1.|) * p1 in halfline (
(0. (TOP-REAL n)),
p1)
by A51, A54, A58, A59, A60;
(1 - (1 / |.p2.|)) * (0. (TOP-REAL n)) = 0. (TOP-REAL n)
;
then
(1 / |.p2.|) * p2 in halfline (
(0. (TOP-REAL n)),
p2)
by A58;
then halfline (
(0. (TOP-REAL n)),
p2) =
halfline (
(0. (TOP-REAL n)),
((1 / |.p1.|) * p1))
by A51, A54, A57, A59, A60, TOPREAL9:31
.=
halfline (
(0. (TOP-REAL n)),
p1)
by A51, A54, A57, A59, A60, A61, TOPREAL9:31
;
then
p1 in halfline (
(0. (TOP-REAL n)),
p2)
by TOPREAL9:28;
then
p1 in {q}
by A37, A49, A55, XBOOLE_0:def 4;
hence
x1 = x2
by A56, TARSKI:def 1;
verum
end;
then A62:
H is one-to-one
by FUNCT_1:def 4;
then
H is being_homeomorphism
by A2, A18, A47, A48, COMPTS_1:17, PRE_TOPC:27;
then reconsider H1 = H " as continuous Function of ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))),(((TOP-REAL n) | cTR0) | FrA) by TOPS_2:def 5;
reconsider HH = H as Function ;
set nN0F = nN0 | (((TOP-REAL n) | cTR0) | FrA);
reconsider H1B = H1 * B as Function of ((TOP-REAL n) | cTR0),(((TOP-REAL n) | cTR0) | FrA) by A47;
reconsider NH1B = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) * H1B as Function of ((TOP-REAL n) | cTR0),R^1 ;
A63:
nN0 | (((TOP-REAL n) | cTR0) | FrA) = nN0 | the carrier of (((TOP-REAL n) | cTR0) | FrA)
by TMAP_1:def 4;
then
( rng NH1B c= rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) & rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) c= rng nN0 )
by RELAT_1:26, RELAT_1:70;
then
rng NH1B c= rng nN0
;
then A64:
not 0 in rng NH1B
;
( B is continuous & not Sphere ((0. (TOP-REAL n)),1) is empty )
by A27, PRE_TOPC:27;
then reconsider NH1B = NH1B as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by A64, RELAT_1:def 9;
reconsider G = I </> NH1B as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;
A65:
dom G = cTR0
by A10, FUNCT_2:def 1;
A66:
dom (nN0 | (((TOP-REAL n) | cTR0) | FrA)) = FrA
by A37, FUNCT_2:def 1;
A67:
for p being Point of (TOP-REAL n) st p in cTR0 holds
ex Hp being Point of (TOP-REAL n) st
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 )
proof
let p be
Point of
(TOP-REAL n);
( p in cTR0 implies ex Hp being Point of (TOP-REAL n) st
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) )
assume A68:
p in cTR0
;
ex Hp being Point of (TOP-REAL n) st
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 )
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
;
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 )
thus
(
Hp = H1B . p &
Hp in FrA )
by A37, A70;
( G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 )
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
;
|.Hp.| > 0
|.Hp.| <> 0
by A63, A69, A70, A73, A72, FUNCT_1:49;
hence
|.Hp.| > 0
;
verum
end;
A74:
not 0. (TOP-REAL n) in rng G
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
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);
( p in cTR0 implies (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} )
assume A84:
p in cTR0
;
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)}
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;
verum
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 ;
( x1 in dom G & x2 in dom G & G . x1 = G . x2 implies x1 = x2 )
assume that A94:
x1 in dom G
and A95:
x2 in dom G
and A96:
G . x1 = G . x2
;
x1 = x2
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;
verum
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);
( p in cTR0 & Hp1 = H1B . p implies ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) )
assume that A107:
p in cTR0
and A108:
Hp1 = H1B . p
;
( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G )
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;
verum
end;
A116:
Sphere ((0. (TOP-REAL n)),1) c= G .: FrA
proof
let p be
object ;
TARSKI:def 3 ( not p in Sphere ((0. (TOP-REAL n)),1) or p in G .: FrA )
assume A117:
p in Sphere (
(0. (TOP-REAL n)),1)
;
p in G .: FrA
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;
verum
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 ;
TARSKI:def 3 ( not y in G .: FrA or y in Sphere ((0. (TOP-REAL n)),1) )
assume
y in G .: FrA
;
y in Sphere ((0. (TOP-REAL n)),1)
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;
verum
end;
set TRnCL = (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1));
set TRnA = (TOP-REAL n) | A;
A137:
Int A c= A
by TOPS_1:16;
set GA = G1 | ((TOP-REAL n) | A);
A138:
G1 | ((TOP-REAL n) | A) = G1 | the carrier of ((TOP-REAL n) | A)
by TMAP_1:def 4;
A139:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
then A140:
dom (G1 | ((TOP-REAL n) | A)) = A
by FUNCT_2:def 1;
A141:
dom (G1 | ((TOP-REAL n) | A)) = the carrier of ((TOP-REAL n) | A)
by FUNCT_2:def 1;
A142:
cl_Ball ((0. (TOP-REAL n)),1) c= rng (G1 | ((TOP-REAL n) | A))
proof
let p be
object ;
TARSKI:def 3 ( not p in cl_Ball ((0. (TOP-REAL n)),1) or p in rng (G1 | ((TOP-REAL n) | A)) )
assume A143:
p in cl_Ball (
(0. (TOP-REAL n)),1)
;
p in rng (G1 | ((TOP-REAL n) | A))
then reconsider p =
p as
Point of
(TOP-REAL n) ;
per cases
( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) )
;
suppose
p = 0. (TOP-REAL n)
;
p in rng (G1 | ((TOP-REAL n) | A))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;
verum end; suppose A144:
p <> 0. (TOP-REAL n)
;
p in rng (G1 | ((TOP-REAL n) | A))set h =
halfline (
(0. (TOP-REAL n)),
p);
A145:
p in cTR0
by A144, ZFMISC_1:56;
then consider Hp being
Point of
(TOP-REAL n) such that A146:
Hp = H1B . p
and A147:
Hp in FrA
and
G . p = (1 / |.Hp.|) * p
and A148:
|.Hp.| > 0
by A67;
A149:
|.|.Hp.|.| = |.Hp.|
by ABSVALUE:def 1;
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp}
by A83, A145, A146;
then
Hp in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p))
by TARSKI:def 1;
then A150:
Hp in halfline (
(0. (TOP-REAL n)),
p)
by XBOOLE_0:def 4;
Hp <> 0. (TOP-REAL n)
by A148, TOPRNS_1:23;
then
halfline (
(0. (TOP-REAL n)),
p)
= halfline (
(0. (TOP-REAL n)),
Hp)
by A150, TOPREAL9:31;
then A151:
|.p.| * Hp in halfline (
(0. (TOP-REAL n)),
p)
by Lm2;
|.p.| <= 1
by A143, TOPREAL9:11;
then
(
(1 - |.p.|) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) &
(|.p.| * Hp) + ((1 - |.p.|) * (0. (TOP-REAL n))) in A )
by A3, A137, A5, A17, A147, RLTOPSP1:def 1;
then
|.p.| * Hp in dom (G1 | ((TOP-REAL n) | A))
by A140;
then A152:
(
(G1 | ((TOP-REAL n) | A)) . (|.p.| * Hp) in rng (G1 | ((TOP-REAL n) | A)) &
(G1 | ((TOP-REAL n) | A)) . (|.p.| * Hp) = G1 . (|.p.| * Hp) )
by A138, FUNCT_1:47, FUNCT_1:def 3;
A153:
|.Hp.| * p in halfline (
(0. (TOP-REAL n)),
p)
by Lm2;
|.Hp.| * p in dom G
by A106, A145, A146;
then
|.Hp.| * p <> 0. (TOP-REAL n)
by A10, ZFMISC_1:56;
then
not
|.Hp.| * p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))
by TARSKI:def 1;
then A154:
G . (|.Hp.| * p) = G1 . (|.Hp.| * p)
by FUNCT_4:11;
|.|.p.|.| = |.p.|
by ABSVALUE:def 1;
then |.(|.p.| * Hp).| =
|.p.| * |.Hp.|
by TOPRNS_1:7
.=
|.(|.Hp.| * p).|
by A149, TOPRNS_1:7
;
then A155:
|.((|.p.| * Hp) - (0. (TOP-REAL n))).| =
|.(|.Hp.| * p).|
.=
|.((|.Hp.| * p) - (0. (TOP-REAL n))).|
;
p = G . (|.Hp.| * p)
by A106, A145, A146;
hence
p in rng (G1 | ((TOP-REAL n) | A))
by A151, A154, A155, A152, A153, Th2;
verum end; end;
end;
rng (G1 | ((TOP-REAL n) | A)) c= cl_Ball ((0. (TOP-REAL n)),1)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (G1 | ((TOP-REAL n) | A)) or x in cl_Ball ((0. (TOP-REAL n)),1) )
assume
x in rng (G1 | ((TOP-REAL n) | A))
;
x in cl_Ball ((0. (TOP-REAL n)),1)
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
( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) )
;
suppose A160:
p <> 0. (TOP-REAL n)
;
x in cl_Ball ((0. (TOP-REAL n)),1)set h =
halfline (
(0. (TOP-REAL n)),
p);
A161:
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;
F is
bounded
by A12, A161, HAUSDORF:18, TBSP_1:14;
then
A /\ (halfline ((0. (TOP-REAL n)),p)) is
bounded
by JORDAN2C:11;
then consider w being
Point of
(Euclid n) such that A162:
w in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p))
and A163:
for
u,
P being
Point of
(Euclid n) st
P = 0. (TOP-REAL n) &
u in A /\ (halfline ((0. (TOP-REAL n)),p)) holds
dist (
P,
u)
<= dist (
P,
w)
and
for
r being
Real st
r > 0 holds
ex
u being
Point of
(Euclid n) st
(
u in A /\ (halfline ((0. (TOP-REAL n)),p)) &
dist (
w,
u)
< r )
by A3, A137, A5, A160, Lm3;
reconsider P =
p as
Point of
(Euclid n) by EUCLID:67;
p in halfline (
(0. (TOP-REAL n)),
p)
by TOPREAL9:28;
then A164:
p in A /\ (halfline ((0. (TOP-REAL n)),p))
by A139, A156, XBOOLE_0:def 4;
A165:
not
p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))
by A160, TARSKI:def 1;
A166:
p in cTR0
by A160, ZFMISC_1:56;
then consider Hp being
Point of
(TOP-REAL n) such that A167:
Hp = H1B . p
and
Hp in FrA
and A168:
G . p = (1 / |.Hp.|) * p
and
|.Hp.| > 0
by A67;
|.(1 / |.Hp.|).| = 1
/ |.Hp.|
by ABSVALUE:def 1;
then A169:
|.((1 / |.Hp.|) * p).| = |.p.| / |.Hp.|
by TOPRNS_1:7;
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp}
by A83, A166, A167;
then
w = Hp
by A162, TARSKI:def 1;
then A170:
dist (
0TRn,
w) =
|.((0. (TOP-REAL n)) - Hp).|
by SPPOL_1:39
.=
|.(- Hp).|
.=
|.Hp.|
by TOPRNS_1:26
;
dist (
0TRn,
P) =
|.((0. (TOP-REAL n)) - p).|
by SPPOL_1:39
.=
|.(- p).|
.=
|.p.|
by TOPRNS_1:26
;
then
|.((1 / |.Hp.|) * p).| <= 1
by A163, A164, A169, A170, XREAL_1:183;
then
|.(G1 . p).| <= 1
by A165, A168, FUNCT_4:11;
hence
x in cl_Ball (
(0. (TOP-REAL n)),1)
by A157, A158, A159;
verum end; end;
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);
BORSUK_1:def 1 for b1 being a_neighborhood of G1 . x ex b2 being a_neighborhood of x st G1 .: b2 c= b1let U be
a_neighborhood of
G1 . x;
ex b1 being a_neighborhood of x st G1 .: b1 c= U
per cases
( x <> 0. (TOP-REAL n) or x = 0. (TOP-REAL n) )
;
suppose A176:
x <> 0. (TOP-REAL n)
;
ex b1 being a_neighborhood of x st G1 .: b1 c= Uthen 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
b1 being
a_neighborhood of
x st
G1 .: b1 c= U
by A180, XBOOLE_1:1;
verumreconsider U1 =
cTR0 /\ U as
Subset of
((TOP-REAL n) | cTR0) by A10, XBOOLE_1:17;
end; suppose A181:
x = 0. (TOP-REAL n)
;
ex b1 being a_neighborhood of x st G1 .: b1 c= Ureconsider 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
;
G1 .: Bx c= Ulet y be
object ;
TARSKI:def 3 ( not y in G1 .: Bx or y in U )assume A185:
y in G1 .: Bx
;
y in Uthen reconsider p =
y as
Point of
(TOP-REAL n) ;
A186:
Int U c= U
by TOPS_1:16;
per cases
( y = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) )
;
suppose A187:
p <> 0. (TOP-REAL n)
;
y in Uset PP =
((e / 2) / |.p.|) * p;
|.((e / 2) / |.p.|).| = (e / 2) / |.p.|
by A6, ABSVALUE:def 1;
then A188:
|.(((e / 2) / |.p.|) * p).| =
((e / 2) / |.p.|) * |.p.|
by TOPRNS_1:7
.=
(e / 2) * (|.p.| / |.p.|)
.=
(e / 2) * 1
by A187, TOPRNS_1:24, XCMPLX_1:60
.=
e / 2
;
then
|.((((e / 2) / |.p.|) * p) - (0. (TOP-REAL n))).| < e
by A174;
then A189:
((e / 2) / |.p.|) * p in Ball (
(0. (TOP-REAL n)),
e)
;
set h =
halfline (
(0. (TOP-REAL n)),
p);
A190:
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;
F is
bounded
by A12, A190, HAUSDORF:18, TBSP_1:14;
then
A /\ (halfline ((0. (TOP-REAL n)),p)) is
bounded
by JORDAN2C:11;
then consider w being
Point of
(Euclid n) such that A191:
w in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p))
and A192:
for
u,
P being
Point of
(Euclid n) st
P = 0. (TOP-REAL n) &
u in A /\ (halfline ((0. (TOP-REAL n)),p)) holds
dist (
P,
u)
<= dist (
P,
w)
and
for
r being
Real st
r > 0 holds
ex
u being
Point of
(Euclid n) st
(
u in A /\ (halfline ((0. (TOP-REAL n)),p)) &
dist (
w,
u)
< r )
by A3, A137, A5, A187, Lm3;
A193:
p in cTR0
by A187, ZFMISC_1:56;
then consider Hp being
Point of
(TOP-REAL n) such that A194:
Hp = H1B . p
and
Hp in FrA
and
G . p = (1 / |.Hp.|) * p
and A195:
|.Hp.| > 0
by A67;
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp}
by A83, A193, A194;
then
w = Hp
by A191, TARSKI:def 1;
then A196:
dist (
0TRn,
w) =
|.((0. (TOP-REAL n)) - Hp).|
by SPPOL_1:39
.=
|.(- Hp).|
.=
|.Hp.|
by TOPRNS_1:26
;
set Hpp =
|.Hp.| * p;
|.Hp.| * p in dom G
by A106, A193, A194;
then
|.Hp.| * p <> 0. (TOP-REAL n)
by A10, ZFMISC_1:56;
then
not
|.Hp.| * p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))
by TARSKI:def 1;
then A197:
G . (|.Hp.| * p) = G1 . (|.Hp.| * p)
by FUNCT_4:11;
|.Hp.| = |.|.Hp.|.|
by ABSVALUE:def 1;
then A198:
(
Bx = Ball (
(0. (TOP-REAL n)),
(r * (e / 2))) &
|.(|.Hp.| * p).| = |.Hp.| * |.p.| )
by TOPREAL9:13, TOPRNS_1:7;
reconsider pp =
((e / 2) / |.p.|) * p as
Point of
(Euclid n) by EUCLID:67;
consider x being
object such that A199:
x in dom G1
and A200:
x in Bx
and A201:
G1 . x = p
by A185, FUNCT_1:def 6;
(
((e / 2) / |.p.|) * p in halfline (
(0. (TOP-REAL n)),
p) &
Ball (
(0. (TOP-REAL n)),
e)
= Ball (
0TRn,
e) )
by A6, Lm2, TOPREAL9:13;
then A202:
pp in A /\ (halfline ((0. (TOP-REAL n)),p))
by A7, A189, XBOOLE_0:def 4;
dist (
0TRn,
pp) =
|.((0. (TOP-REAL n)) - (((e / 2) / |.p.|) * p)).|
by SPPOL_1:39
.=
|.(- (((e / 2) / |.p.|) * p)).|
.=
e / 2
by A188, TOPRNS_1:26
;
then
(e / 2) / |.Hp.| <= 1
by A192, A196, A202, XREAL_1:183;
then A203:
r * ((e / 2) / |.Hp.|) <= r * 1
by A183, XREAL_1:64;
p = G . (|.Hp.| * p)
by A106, A193, A194;
then
|.Hp.| * p = x
by A105, A197, A199, A201, FUNCT_1:def 4;
then
|.p.| < (r * (e / 2)) / |.Hp.|
by A195, A198, A200, TOPREAL9:10, XREAL_1:81;
then
|.p.| < r
by A203, XXREAL_0:2;
then
|.(p - (0. (TOP-REAL n))).| < r
;
then
p in Ball (
(0. (TOP-REAL n)),
r)
;
then
p in Ball (
0TRn,
r)
by TOPREAL9:13;
hence
y in U
by A184;
verum end; end; end; end;
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; verum