:: BROUWER semantic presentation

REAL is non empty V43() V140() V141() V142() V146() set
NAT is V140() V141() V142() V143() V144() V145() V146() Element of bool REAL
bool REAL is non empty set
K582() is non empty strict TopSpace-like V218() V225() pathwise_connected SubSpace of K580()
K580() is non empty strict TopSpace-like V225() TopStruct
the carrier of K582() is non empty V140() V141() V142() set
[:K582(),K582():] is non empty strict TopSpace-like TopStruct
the carrier of [:K582(),K582():] is non empty set
COMPLEX is non empty V43() V140() V146() set
RAT is non empty V43() V140() V141() V142() V143() V146() set
INT is non empty V43() V140() V141() V142() V143() V144() V146() set
[:COMPLEX,COMPLEX:] is non empty V16() complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V16() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty V16() complex-yielding V131() V132() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V16() complex-yielding V131() V132() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty V16() V20( RAT ) complex-yielding V131() V132() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V16() V20( RAT ) complex-yielding V131() V132() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V131() V132() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V131() V132() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is V16() V20( RAT ) V20( INT ) complex-yielding V131() V132() V133() set
[:[:NAT,NAT:],NAT:] is V16() V20( RAT ) V20( INT ) complex-yielding V131() V132() V133() set
bool [:[:NAT,NAT:],NAT:] is non empty set
omega is V140() V141() V142() V143() V144() V145() V146() set
bool omega is non empty set
bool NAT is non empty set
K401() is non empty non trivial V67() V89() L8()
the carrier of K401() is non empty non trivial V43() set
K406() is non empty V89() V111() V112() V113() V115() V162() V163() V164() V165() V166() V167() L8()
K407() is non empty non trivial V67() V89() V113() V115() V165() V166() V167() M15(K406())
K408() is non empty V89() V111() V113() V115() V165() V166() V167() V168() M18(K406(),K407())
K410() is non empty V89() V111() V113() V115() L8()
K411() is non empty V89() V111() V113() V115() V168() M15(K410())
1 is non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
[:1,1:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V131() V132() V133() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V131() V132() V133() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V16() complex-yielding V131() V132() set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
[:2,2:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V131() V132() V133() set
[:[:2,2:],REAL:] is non empty V16() complex-yielding V131() V132() set
bool [:[:2,2:],REAL:] is non empty set
TOP-REAL 2 is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL 2) is non empty set
{} is empty trivial V16() non-empty empty-yielding V20( RAT ) Function-like one-to-one constant functional complex-yielding V131() V132() V133() V134() V135() V136() V137() V140() V141() V142() V143() V144() V145() V146() set
the empty trivial V16() non-empty empty-yielding V20( RAT ) Function-like one-to-one constant functional complex-yielding V131() V132() V133() V134() V135() V136() V137() V140() V141() V142() V143() V144() V145() V146() set is empty trivial V16() non-empty empty-yielding V20( RAT ) Function-like one-to-one constant functional complex-yielding V131() V132() V133() V134() V135() V136() V137() V140() V141() V142() V143() V144() V145() V146() set
{{},1} is non empty set
I[01] is non empty strict TopSpace-like V218() V225() pathwise_connected TopStruct
the carrier of I[01] is non empty V140() V141() V142() set
K471() is V188() V225() L14()
[:I[01],I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:I[01],I[01]:] is non empty set
[:K580(),K580():] is non empty strict TopSpace-like TopStruct
the carrier of [:K580(),K580():] is non empty set
[: the carrier of [:K580(),K580():], the carrier of (TOP-REAL 2):] is non empty V16() set
bool [: the carrier of [:K580(),K580():], the carrier of (TOP-REAL 2):] is non empty set
R^1 is non empty strict TopSpace-like V225() pathwise_connected V235() SubSpace of K580()
the carrier of R^1 is non empty V140() V141() V142() set
bool the carrier of R^1 is non empty set
bool (bool the carrier of R^1) is non empty set
Tunit_circle 2 is non empty TopSpace-like V236() SubSpace of TOP-REAL 2
the carrier of (Tunit_circle 2) is non empty set
[: the carrier of R^1, the carrier of (Tunit_circle 2):] is non empty V16() set
bool [: the carrier of R^1, the carrier of (Tunit_circle 2):] is non empty set
CircleMap is non empty V16() V19( the carrier of R^1) V19( the carrier of R^1) V20( the carrier of (Tunit_circle 2)) V20( the carrier of (Tunit_circle 2)) Function-like total total quasi_total quasi_total onto continuous Element of bool [: the carrier of R^1, the carrier of (Tunit_circle 2):]
c[10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[10] is non empty strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[10]) is non empty set
0 is empty trivial ordinal natural V11() ext-real non positive non negative real V16() non-empty empty-yielding V20( RAT ) Function-like one-to-one constant functional V33() V34() complex-yielding V131() V132() V133() V134() V135() V136() V137() V140() V141() V142() V143() V144() V145() V146() Element of NAT
].0,1.[ is non empty V140() V141() V142() open Element of bool REAL
R^1 ].0,1.[ is non empty V140() V141() V142() open Element of bool the carrier of R^1
R^1 | (R^1 ].0,1.[) is non empty strict TopSpace-like V225() SubSpace of R^1
the carrier of (R^1 | (R^1 ].0,1.[)) is non empty V140() V141() V142() set
[: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is non empty set
c[-10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[-10] is non empty strict TopSpace-like SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[-10]) is non empty set
1 / 2 is V11() ext-real non negative real Element of REAL
3 is non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
3 / 2 is V11() ext-real non negative real Element of REAL
].(1 / 2),(3 / 2).[ is non empty V140() V141() V142() open Element of bool REAL
R^1 ].(1 / 2),(3 / 2).[ is non empty V140() V141() V142() open Element of bool the carrier of R^1
R^1 | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like V225() SubSpace of R^1
the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)) is non empty V140() V141() V142() set
[: the carrier of (Topen_unit_circle c[-10]), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of (Topen_unit_circle c[-10]), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is non empty set
[: the carrier of K582(), the carrier of K582():] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of K582(), the carrier of K582():] is non empty set
bool the carrier of [:K582(),K582():] is non empty set
[: the carrier of (TOP-REAL 2),REAL:] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of (TOP-REAL 2),REAL:] is non empty set
bool the carrier of (TOP-REAL 2) is non empty set
{0} is non empty trivial functional V140() V141() V142() V143() V144() V145() set
0[01] is V11() ext-real real Element of the carrier of I[01]
1[01] is V11() ext-real real Element of the carrier of I[01]
the carrier of K580() is non empty V140() V141() V142() set
sqrt 0 is V11() ext-real non negative real Element of REAL
4 is non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
sqrt 4 is non empty V11() ext-real positive non negative real Element of REAL
bool the carrier of K580() is non empty set
R2Homeomorphism is non empty V16() V19( the carrier of [:K580(),K580():]) V20( the carrier of (TOP-REAL 2)) Function-like total quasi_total Element of bool [: the carrier of [:K580(),K580():], the carrier of (TOP-REAL 2):]
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
o is non empty TopSpace-like TopStruct
the carrier of o is non empty set
{ [b₁,b₂] where b₁ is Element of the carrier of r, b₂ is Element of the carrier of o : not b₁ = b₂ } is set
[:r,o:] is non empty strict TopSpace-like TopStruct
the carrier of [:r,o:] is non empty set
bool the carrier of [:r,o:] is non empty set
x is set
c₆ is Element of the carrier of r
g is Element of the carrier of o
[c₆,g] is non empty Element of the carrier of [:r,o:]
{c₆,g} is non empty set
{c₆} is non empty trivial set
{{c₆,g},{c₆}} is non empty set
x is non empty TopSpace-like TopStruct
the carrier of x is non empty set
c₆ is non empty TopSpace-like TopStruct
the carrier of c₆ is non empty set
f is set
r is non empty TopSpace-like TopStruct
o is non empty TopSpace-like TopStruct
(r,o) is Element of bool the carrier of [:r,o:]
[:r,o:] is non empty strict TopSpace-like TopStruct
the carrier of [:r,o:] is non empty set
bool the carrier of [:r,o:] is non empty set
the carrier of r is non empty set
the carrier of o is non empty set
{ [b₁,b₂] where b₁ is Element of the carrier of r, b₂ is Element of the carrier of o : not b₁ = b₂ } is set
g is set
W is Element of the carrier of x
yo is Element of the carrier of c₆
[W,yo] is non empty Element of the carrier of [:x,c₆:]
[:x,c₆:] is non empty strict TopSpace-like TopStruct
the carrier of [:x,c₆:] is non empty set
{W,yo} is non empty set
{W} is non empty trivial set
{{W,yo},{W}} is non empty set
(x,c₆) is Element of bool the carrier of [:x,c₆:]
bool the carrier of [:x,c₆:] is non empty set
{ [b₁,b₂] where b₁ is Element of the carrier of x, b₂ is Element of the carrier of c₆ : not b₁ = b₂ } is set
r is non empty non trivial TopSpace-like TopStruct
o is non empty TopSpace-like TopStruct
(r,o) is Element of bool the carrier of [:r,o:]
[:r,o:] is non empty strict TopSpace-like TopStruct
the carrier of [:r,o:] is non empty set
bool the carrier of [:r,o:] is non empty set
the carrier of r is non empty non trivial set
the carrier of o is non empty set
{ [b₁,b₂] where b₁ is Element of the carrier of r, b₂ is Element of the carrier of o : not b₁ = b₂ } is set
the Element of the carrier of o is Element of the carrier of o
x is Element of the carrier of r
c₆ is Element of the carrier of r
[c₆, the Element of the carrier of o] is non empty Element of the carrier of [:r,o:]
{c₆, the Element of the carrier of o} is non empty set
{c₆} is non empty trivial set
{{c₆, the Element of the carrier of o},{c₆}} is non empty set
[x, the Element of the carrier of o] is non empty Element of the carrier of [:r,o:]
{x, the Element of the carrier of o} is non empty set
{x} is non empty trivial set
{{x, the Element of the carrier of o},{x}} is non empty set
r is non empty TopSpace-like TopStruct
o is non empty non trivial TopSpace-like TopStruct
(r,o) is Element of bool the carrier of [:r,o:]
[:r,o:] is non empty strict TopSpace-like TopStruct
the carrier of [:r,o:] is non empty set
bool the carrier of [:r,o:] is non empty set
the carrier of r is non empty set
the carrier of o is non empty non trivial set
{ [b₁,b₂] where b₁ is Element of the carrier of r, b₂ is Element of the carrier of o : not b₁ = b₂ } is set
the Element of the carrier of r is Element of the carrier of r
x is Element of the carrier of o
c₆ is Element of the carrier of o
[ the Element of the carrier of r,c₆] is non empty Element of the carrier of [:r,o:]
{ the Element of the carrier of r,c₆} is non empty set
{ the Element of the carrier of r} is non empty trivial set
{{ the Element of the carrier of r,c₆},{ the Element of the carrier of r}} is non empty set
[ the Element of the carrier of r,x] is non empty Element of the carrier of [:r,o:]
{ the Element of the carrier of r,x} is non empty set
{ the Element of the carrier of r} is non empty trivial set
{{ the Element of the carrier of r,x},{ the Element of the carrier of r}} is non empty set
r is ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
cl_Ball (o,0) is non empty closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
{o} is non empty trivial functional set
f is set
x is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
x - o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- o is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL r),x,(- o)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
x + (- o) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - o is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.(x - o).| is V11() ext-real non negative real Element of REAL
f is set
o - o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- o is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL r),o,(- o)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
o + (- o) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
o - o is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.(o - o).| is V11() ext-real non negative real Element of REAL
r is ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
f is V11() ext-real real set
cl_Ball (o,f) is closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
(TOP-REAL r) | (cl_Ball (o,f)) is strict TopSpace-like SubSpace of TOP-REAL r
r is ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
f is V11() ext-real non negative real set
(r,o,f) is TopSpace-like SubSpace of TOP-REAL r
cl_Ball (o,f) is non empty closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
(TOP-REAL r) | (cl_Ball (o,f)) is non empty strict TopSpace-like SubSpace of TOP-REAL r
r is ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
o is V11() ext-real real set
f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
(r,f,o) is TopSpace-like SubSpace of TOP-REAL r
cl_Ball (f,o) is closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
(TOP-REAL r) | (cl_Ball (f,o)) is strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (r,f,o) is set
[#] (r,f,o) is non proper open closed Element of bool the carrier of (r,f,o)
bool the carrier of (r,f,o) is non empty set
r is ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
f is V11() ext-real real set
(r,o,f) is TopSpace-like SubSpace of TOP-REAL r
cl_Ball (o,f) is closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
(TOP-REAL r) | (cl_Ball (o,f)) is strict TopSpace-like SubSpace of TOP-REAL r
[#] (r,o,f) is non proper open closed Element of bool the carrier of (r,o,f)
the carrier of (r,o,f) is set
bool the carrier of (r,o,f) is non empty set
r is ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
o is V11() ext-real non negative real set
f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
x is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
halfline (f,x) is non empty convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
c₆ is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
(r,c₆,o) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL r
cl_Ball (c₆,o) is non empty closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
(TOP-REAL r) | (cl_Ball (c₆,o)) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (r,c₆,o) is non empty set
Tcircle (c₆,o) is TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (c₆,o)) is set
Sphere (c₆,o) is closed V217( TOP-REAL r) Element of bool the carrier of (TOP-REAL r)
(halfline (f,x)) /\ (Sphere (c₆,o)) is Element of bool the carrier of (TOP-REAL r)
REAL r is non empty V53() M12( REAL )
x - f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- f is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL r),x,(- f)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
x + (- f) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - f is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
f - c₆ is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- c₆ is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL r),f,(- c₆)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
f + (- c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
f - c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|((x - f),(f - c₆))| is V11() ext-real real Element of REAL
2 * |((x - f),(f - c₆))| is V11() ext-real real Element of REAL
- (2 * |((x - f),(f - c₆))|) is V11() ext-real real Element of REAL
W is V50(r) Element of REAL r
g is V50(r) Element of REAL r
W - g is V16() V19( NAT ) V20( REAL ) Function-like V50(r) V51() complex-yielding V131() V132() M13( REAL , REAL r)
sqr (W - g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M13( REAL ,K373(r,REAL))
K373(r,REAL) is V53() M12( REAL )
Sum (sqr (W - g)) is V11() ext-real real Element of REAL
yo is V50(r) Element of REAL r
g - yo is V16() V19( NAT ) V20( REAL ) Function-like V50(r) V51() complex-yielding V131() V132() M13( REAL , REAL r)
sqr (g - yo) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M13( REAL ,K373(r,REAL))
Sum (sqr (g - yo)) is V11() ext-real real Element of REAL
o ^2 is V11() ext-real real set
o * o is V11() ext-real non negative real set
(Sum (sqr (g - yo))) - (o ^2) is V11() ext-real real Element of REAL
delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2))) is V11() ext-real real Element of REAL
sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))) is V11() ext-real real Element of REAL
(- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2))))) is V11() ext-real real Element of REAL
2 * (Sum (sqr (W - g))) is V11() ext-real real Element of REAL
((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))) is V11() ext-real real Element of REAL
|.(f - c₆).| is V11() ext-real non negative real Element of REAL
Ball (c₆,o) is open V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) is V11() ext-real real Element of REAL
(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
the U10 of (TOP-REAL r) is non empty V16() V19([:REAL, the carrier of (TOP-REAL r):]) V20( the carrier of (TOP-REAL r)) Function-like total quasi_total Element of bool [:[:REAL, the carrier of (TOP-REAL r):], the carrier of (TOP-REAL r):]
[:REAL, the carrier of (TOP-REAL r):] is non empty V16() set
[:[:REAL, the carrier of (TOP-REAL r):], the carrier of (TOP-REAL r):] is non empty V16() set
bool [:[:REAL, the carrier of (TOP-REAL r):], the carrier of (TOP-REAL r):] is non empty set
the U10 of (TOP-REAL r) . ((1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),f) is set
[(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),f] is non empty set
{(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),f} is non empty set
{(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))))} is non empty trivial V140() V141() V142() set
{{(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),f},{(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))))}} is non empty set
the U10 of (TOP-REAL r) . [(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),f] is set
(1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * f is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
the U10 of (TOP-REAL r) . ((((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x) is set
[(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x] is non empty set
{(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x} is non empty set
{(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))} is non empty trivial V140() V141() V142() set
{{(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x},{(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))}} is non empty set
the U10 of (TOP-REAL r) . [(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x] is set
(((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * f) + ((((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
((1 - (((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * f) + ((((- (2 * |((x - f),(f - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - f),(f - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
D2 is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
{D2} is non empty trivial functional set
r is ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
o is V11() ext-real non negative real set
f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
x is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
halfline (f,x) is non empty convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
c₆ is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
Tcircle (c₆,o) is TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (c₆,o)) is set
(r,c₆,o) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL r
cl_Ball (c₆,o) is non empty closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
(TOP-REAL r) | (cl_Ball (c₆,o)) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (r,c₆,o) is non empty set
Sphere (c₆,o) is closed V217( TOP-REAL r) Element of bool the carrier of (TOP-REAL r)
(halfline (f,x)) /\ (Sphere (c₆,o)) is Element of bool the carrier of (TOP-REAL r)
REAL r is non empty V53() M12( REAL )
(1 / 2) * f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
the U10 of (TOP-REAL r) is non empty V16() V19([:REAL, the carrier of (TOP-REAL r):]) V20( the carrier of (TOP-REAL r)) Function-like total quasi_total Element of bool [:[:REAL, the carrier of (TOP-REAL r):], the carrier of (TOP-REAL r):]
[:REAL, the carrier of (TOP-REAL r):] is non empty V16() set
[:[:REAL, the carrier of (TOP-REAL r):], the carrier of (TOP-REAL r):] is non empty V16() set
bool [:[:REAL, the carrier of (TOP-REAL r):], the carrier of (TOP-REAL r):] is non empty set
the U10 of (TOP-REAL r) . ((1 / 2),f) is set
[(1 / 2),f] is non empty set
{(1 / 2),f} is non empty set
{(1 / 2)} is non empty trivial V140() V141() V142() set
{{(1 / 2),f},{(1 / 2)}} is non empty set
the U10 of (TOP-REAL r) . [(1 / 2),f] is set
(1 / 2) * f is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(1 / 2) * x is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
the U10 of (TOP-REAL r) . ((1 / 2),x) is set
[(1 / 2),x] is non empty set
{(1 / 2),x} is non empty set
{{(1 / 2),x},{(1 / 2)}} is non empty set
the U10 of (TOP-REAL r) . [(1 / 2),x] is set
(1 / 2) * x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 / 2) * f) + ((1 / 2) * x) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
((1 / 2) * f) + ((1 / 2) * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - (((1 / 2) * f) + ((1 / 2) * x)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- (((1 / 2) * f) + ((1 / 2) * x)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- (((1 / 2) * f) + ((1 / 2) * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL r),x,(- (((1 / 2) * f) + ((1 / 2) * x)))) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
x + (- (((1 / 2) * f) + ((1 / 2) * x))) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - (((1 / 2) * f) + ((1 / 2) * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((1 / 2) * f) + ((1 / 2) * x)) - c₆ is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- c₆ is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
- c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL r),(((1 / 2) * f) + ((1 / 2) * x)),(- c₆)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
(((1 / 2) * f) + ((1 / 2) * x)) + (- c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((1 / 2) * f) + ((1 / 2) * x)) - c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))| is V11() ext-real real Element of REAL
2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))| is V11() ext-real real Element of REAL
- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|) is V11() ext-real real Element of REAL
W is V50(r) Element of REAL r
g is V50(r) Element of REAL r
W - g is V16() V19( NAT ) V20( REAL ) Function-like V50(r) V51() complex-yielding V131() V132() M13( REAL , REAL r)
sqr (W - g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M13( REAL ,K373(r,REAL))
K373(r,REAL) is V53() M12( REAL )
Sum (sqr (W - g)) is V11() ext-real real Element of REAL
yo is V50(r) Element of REAL r
g - yo is V16() V19( NAT ) V20( REAL ) Function-like V50(r) V51() complex-yielding V131() V132() M13( REAL , REAL r)
sqr (g - yo) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M13( REAL ,K373(r,REAL))
Sum (sqr (g - yo)) is V11() ext-real real Element of REAL
o ^2 is V11() ext-real real set
o * o is V11() ext-real non negative real set
(Sum (sqr (g - yo))) - (o ^2) is V11() ext-real real Element of REAL
delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2))) is V11() ext-real real Element of REAL
sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))) is V11() ext-real real Element of REAL
(- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2))))) is V11() ext-real real Element of REAL
2 * (Sum (sqr (W - g))) is V11() ext-real real Element of REAL
((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))) is V11() ext-real real Element of REAL
1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) is V11() ext-real real Element of REAL
(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * (((1 / 2) * f) + ((1 / 2) * x)) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
the U10 of (TOP-REAL r) . ((1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),(((1 / 2) * f) + ((1 / 2) * x))) is set
[(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),(((1 / 2) * f) + ((1 / 2) * x))] is non empty set
{(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),(((1 / 2) * f) + ((1 / 2) * x))} is non empty set
{(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))))} is non empty trivial V140() V141() V142() set
{{(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),(((1 / 2) * f) + ((1 / 2) * x))},{(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))))}} is non empty set
the U10 of (TOP-REAL r) . [(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))),(((1 / 2) * f) + ((1 / 2) * x))] is set
(1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * (((1 / 2) * f) + ((1 / 2) * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
the U10 of (TOP-REAL r) . ((((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x) is set
[(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x] is non empty set
{(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x} is non empty set
{(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))} is non empty trivial V140() V141() V142() set
{{(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x},{(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))}} is non empty set
the U10 of (TOP-REAL r) . [(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))),x] is set
(((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * (((1 / 2) * f) + ((1 / 2) * x))) + ((((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
((1 - (((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g)))))) * (((1 / 2) * f) + ((1 / 2) * x))) + ((((- (2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|)) + (sqrt (delta ((Sum (sqr (W - g))),(2 * |((x - (((1 / 2) * f) + ((1 / 2) * x))),((((1 / 2) * f) + ((1 / 2) * x)) - c₆))|),((Sum (sqr (g - yo))) - (o ^2)))))) / (2 * (Sum (sqr (W - g))))) * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
D2 is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
{f,D2} is non empty functional set
r is non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL r is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL r) is non empty set
f is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
o is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
c₆ is V11() ext-real non negative real set
(r,o,c₆) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL r
cl_Ball (o,c₆) is non empty closed V217( TOP-REAL r) convex Element of bool the carrier of (TOP-REAL r)
bool the carrier of (TOP-REAL r) is non empty set
(TOP-REAL r) | (cl_Ball (o,c₆)) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (r,o,c₆) is non empty set
x is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
halfline (f,x) is non empty convex Element of bool the carrier of (TOP-REAL r)
Sphere (o,c₆) is non empty closed V217( TOP-REAL r) Element of bool the carrier of (TOP-REAL r)
(halfline (f,x)) /\ (Sphere (o,c₆)) is Element of bool the carrier of (TOP-REAL r)
Tcircle (o,c₆) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (o,c₆)) is non empty set
g is Element of the carrier of (Tcircle (o,c₆))
{f,g} is non empty set
W is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
Tcircle (o,c₆) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (o,c₆)) is non empty set
g is Element of the carrier of (Tcircle (o,c₆))
{g} is non empty trivial set
W is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
Tcircle (o,c₆) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (o,c₆)) is non empty set
g is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
W is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
Tcircle (o,c₆) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (o,c₆)) is non empty set
yo is Element of the carrier of (Tcircle (o,c₆))
{f,yo} is non empty set
Tcircle (o,c₆) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (o,c₆)) is non empty set
yo is Element of the carrier of (Tcircle (o,c₆))
{yo} is non empty trivial set
Tcircle (o,c₆) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (o,c₆)) is non empty set
r is V11() ext-real non negative real set
o is non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL o is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL o) is non empty set
f is V16() Function-like V50(o) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL o)
x is V16() Function-like V50(o) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL o)
(o,x,r) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL o
cl_Ball (x,r) is non empty closed V217( TOP-REAL o) convex Element of bool the carrier of (TOP-REAL o)
bool the carrier of (TOP-REAL o) is non empty set
(TOP-REAL o) | (cl_Ball (x,r)) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (o,x,r) is non empty set
Tcircle (x,r) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (Tcircle (x,r)) is non empty set
c₆ is V16() Function-like V50(o) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL o)
(o,x,f,c₆,r) is V16() Function-like V50(o) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL o)
Sphere (x,r) is non empty closed V217( TOP-REAL o) Element of bool the carrier of (TOP-REAL o)
halfline (f,c₆) is non empty convex Element of bool the carrier of (TOP-REAL o)
(halfline (f,c₆)) /\ (Sphere (x,r)) is Element of bool the carrier of (TOP-REAL o)
r is V11() ext-real real set
1 - r is V11() ext-real real Element of REAL
o is V11() ext-real non negative real set
o ^2 is V11() ext-real real set
o * o is V11() ext-real non negative real set
f is non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() Element of NAT
TOP-REAL f is non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() L16()
the carrier of (TOP-REAL f) is non empty set
REAL f is non empty V53() M12( REAL )
x is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(1 - r) * x is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
the U10 of (TOP-REAL f) is non empty V16() V19([:REAL, the carrier of (TOP-REAL f):]) V20( the carrier of (TOP-REAL f)) Function-like total quasi_total Element of bool [:[:REAL, the carrier of (TOP-REAL f):], the carrier of (TOP-REAL f):]
[:REAL, the carrier of (TOP-REAL f):] is non empty V16() set
[:[:REAL, the carrier of (TOP-REAL f):], the carrier of (TOP-REAL f):] is non empty V16() set
bool [:[:REAL, the carrier of (TOP-REAL f):], the carrier of (TOP-REAL f):] is non empty set
the U10 of (TOP-REAL f) . ((1 - r),x) is set
[(1 - r),x] is non empty set
{(1 - r),x} is non empty set
{(1 - r)} is non empty trivial V140() V141() V142() set
{{(1 - r),x},{(1 - r)}} is non empty set
the U10 of (TOP-REAL f) . [(1 - r),x] is set
(1 - r) * x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
c₆ is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
c₆ - x is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- x is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL f),c₆,(- x)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
c₆ + (- x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
c₆ - x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
r * c₆ is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
the U10 of (TOP-REAL f) . (r,c₆) is set
[r,c₆] is non empty set
{r,c₆} is non empty set
{r} is non empty trivial V140() V141() V142() set
{{r,c₆},{r}} is non empty set
the U10 of (TOP-REAL f) . [r,c₆] is set
r * c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 - r) * x) + (r * c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
((1 - r) * x) + (r * c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
g is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(f,g,o) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL f
cl_Ball (g,o) is non empty closed V217( TOP-REAL f) convex Element of bool the carrier of (TOP-REAL f)
bool the carrier of (TOP-REAL f) is non empty set
(TOP-REAL f) | (cl_Ball (g,o)) is non empty strict TopSpace-like SubSpace of TOP-REAL f
the carrier of (f,g,o) is non empty set
x - g is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- g is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- g is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL f),x,(- g)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (- g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - g is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|((c₆ - x),(x - g))| is V11() ext-real real Element of REAL
- |((c₆ - x),(x - g))| is V11() ext-real real