:: 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 Element of REAL
|((c₆ - x),(x - g))| ^2 is V11() ext-real real Element of REAL
|((c₆ - x),(x - g))| * |((c₆ - x),(x - g))| is V11() ext-real non negative real set
(f,g,x,c₆,o) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
W is V50(f) Element of REAL f
yo is V50(f) Element of REAL f
f1 is V50(f) Element of REAL f
yo - W is V16() V19( NAT ) V20( REAL ) Function-like V50(f) V51() complex-yielding V131() V132() M13( REAL , REAL f)
sqr (yo - W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M13( REAL ,K373(f,REAL))
K373(f,REAL) is V53() M12( REAL )
Sum (sqr (yo - W)) is V11() ext-real real Element of REAL
W - f1 is V16() V19( NAT ) V20( REAL ) Function-like V50(f) V51() complex-yielding V131() V132() M13( REAL , REAL f)
sqr (W - f1) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M13( REAL ,K373(f,REAL))
Sum (sqr (W - f1)) is V11() ext-real real Element of REAL
(Sum (sqr (W - f1))) - (o ^2) is V11() ext-real real Element of REAL
(Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2)) is V11() ext-real real Element of REAL
(|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2))) is V11() ext-real real Element of REAL
sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2)))) is V11() ext-real real Element of REAL
(- |((c₆ - x),(x - g))|) + (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2))))) is V11() ext-real real Element of REAL
((- |((c₆ - x),(x - g))|) + (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2)))))) / (Sum (sqr (yo - W))) is V11() ext-real real Element of REAL
|.(yo - W).| is V11() ext-real non negative real Element of REAL
sqrt (Sum (sqr (yo - W))) is V11() ext-real real Element of REAL
halfline (x,c₆) is non empty convex Element of bool the carrier of (TOP-REAL f)
Sphere (g,o) is non empty closed V217( TOP-REAL f) Element of bool the carrier of (TOP-REAL f)
(halfline (x,c₆)) /\ (Sphere (g,o)) is Element of bool the carrier of (TOP-REAL f)
S1 is V11() ext-real real set
1 - S1 is V11() ext-real real Element of REAL
(1 - S1) * 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) . ((1 - S1),x) is set
[(1 - S1),x] is non empty set
{(1 - S1),x} is non empty set
{(1 - S1)} is non empty trivial V140() V141() V142() set
{{(1 - S1),x},{(1 - S1)}} is non empty set
the U10 of (TOP-REAL f) . [(1 - S1),x] is set
(1 - S1) * x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
S1 * 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) . (S1,c₆) is set
[S1,c₆] is non empty set
{S1,c₆} is non empty set
{S1} is non empty trivial V140() V141() V142() set
{{S1,c₆},{S1}} is non empty set
the U10 of (TOP-REAL f) . [S1,c₆] is set
S1 * c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 - S1) * x) + (S1 * c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
((1 - S1) * x) + (S1 * c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((1 - S1) * x) + (S1 * c₆)) - g is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),(((1 - S1) * x) + (S1 * c₆)),(- g)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(((1 - S1) * x) + (S1 * c₆)) + (- g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((1 - S1) * x) + (S1 * c₆)) - g is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((((1 - S1) * x) + (S1 * c₆)) - g).| is V11() ext-real non negative real Element of REAL
1 * 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) . (1,x) is set
[1,x] is non empty set
{1,x} is non empty set
{1} is non empty trivial V140() V141() V142() V143() V144() V145() set
{{1,x},{1}} is non empty set
the U10 of (TOP-REAL f) . [1,x] is set
1 * x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
S1 * 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) . (S1,x) is set
[S1,x] is non empty set
{S1,x} is non empty set
{{S1,x},{S1}} is non empty set
the U10 of (TOP-REAL f) . [S1,x] is set
S1 * x is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(1 * x) - (S1 * x) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- (S1 * x) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- (S1 * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL f),(1 * x),(- (S1 * x))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(1 * x) + (- (S1 * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(1 * x) - (S1 * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 * x) - (S1 * x)) + (S1 * c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
((1 * x) - (S1 * x)) + (S1 * c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((1 * x) - (S1 * x)) + (S1 * c₆)) - g is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),(((1 * x) - (S1 * x)) + (S1 * c₆)),(- g)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(((1 * x) - (S1 * x)) + (S1 * c₆)) + (- g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(((1 * x) - (S1 * x)) + (S1 * c₆)) - g is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((((1 * x) - (S1 * x)) + (S1 * c₆)) - g).| is V11() ext-real non negative real Element of REAL
x - (S1 * x) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),x,(- (S1 * x))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (- (S1 * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - (S1 * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x - (S1 * x)) + (S1 * c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x - (S1 * x)) + (S1 * c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((x - (S1 * x)) + (S1 * c₆)) - g is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),((x - (S1 * x)) + (S1 * c₆)),(- g)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
((x - (S1 * x)) + (S1 * c₆)) + (- g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((x - (S1 * x)) + (S1 * c₆)) - g is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.(((x - (S1 * x)) + (S1 * c₆)) - g).| is V11() ext-real non negative real Element of REAL
(S1 * x) - (S1 * c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- (S1 * c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- (S1 * c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL f),(S1 * x),(- (S1 * c₆))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(S1 * x) + (- (S1 * c₆)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(S1 * x) - (S1 * c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - ((S1 * x) - (S1 * c₆)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- ((S1 * x) - (S1 * c₆)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- ((S1 * x) - (S1 * c₆)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL f),x,(- ((S1 * x) - (S1 * c₆)))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (- ((S1 * x) - (S1 * c₆))) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - ((S1 * x) - (S1 * c₆)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x - ((S1 * x) - (S1 * c₆))) - g is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),(x - ((S1 * x) - (S1 * c₆))),(- g)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x - ((S1 * x) - (S1 * c₆))) + (- g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x - ((S1 * x) - (S1 * c₆))) - g is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((x - ((S1 * x) - (S1 * c₆))) - g).| is V11() ext-real non negative real Element of REAL
x + (- ((S1 * x) - (S1 * c₆))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x + (- ((S1 * x) - (S1 * c₆)))) + (- g) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x + (- ((S1 * x) - (S1 * c₆)))) + (- g) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((x + (- ((S1 * x) - (S1 * c₆)))) + (- g)).| is V11() ext-real non negative real Element of REAL
x + (- g) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x + (- g)) + (- ((S1 * x) - (S1 * c₆))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x + (- g)) + (- ((S1 * x) - (S1 * c₆))) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((x + (- g)) + (- ((S1 * x) - (S1 * c₆)))).| is V11() ext-real non negative real Element of REAL
(x - g) - ((S1 * x) - (S1 * c₆)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),(x - g),(- ((S1 * x) - (S1 * c₆)))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x - g) + (- ((S1 * x) - (S1 * c₆))) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x - g) - ((S1 * x) - (S1 * c₆)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((x - g) - ((S1 * x) - (S1 * c₆))).| is V11() ext-real non negative real Element of REAL
x - c₆ is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- c₆ is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL f),x,(- c₆)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (- c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x - c₆ is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
S1 * (x - 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) . (S1,(x - c₆)) is set
[S1,(x - c₆)] is non empty set
{S1,(x - c₆)} is non empty set
{{S1,(x - c₆)},{S1}} is non empty set
the U10 of (TOP-REAL f) . [S1,(x - c₆)] is set
S1 * (x - c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
- (S1 * (x - c₆)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- (S1 * (x - c₆)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x - g) + (- (S1 * (x - c₆))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x - g) + (- (S1 * (x - c₆))) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((x - g) + (- (S1 * (x - c₆)))).| is V11() ext-real non negative real Element of REAL
- (x - c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
- (x - c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
S1 * (- (x - 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) . (S1,(- (x - c₆))) is set
[S1,(- (x - c₆))] is non empty set
{S1,(- (x - c₆))} is non empty set
{{S1,(- (x - c₆))},{S1}} is non empty set
the U10 of (TOP-REAL f) . [S1,(- (x - c₆))] is set
S1 * (- (x - c₆)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x - g) + (S1 * (- (x - c₆))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x - g) + (S1 * (- (x - c₆))) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((x - g) + (S1 * (- (x - c₆)))).| is V11() ext-real non negative real Element of REAL
S1 * (c₆ - 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) . (S1,(c₆ - x)) is set
[S1,(c₆ - x)] is non empty set
{S1,(c₆ - x)} is non empty set
{{S1,(c₆ - x)},{S1}} is non empty set
the U10 of (TOP-REAL f) . [S1,(c₆ - x)] is set
S1 * (c₆ - x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x - g) + (S1 * (c₆ - x)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x - g) + (S1 * (c₆ - x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((x - g) + (S1 * (c₆ - x))).| is V11() ext-real non negative real Element of REAL
|.(x - g).| is V11() ext-real non negative real Element of REAL
|.(x - g).| ^2 is V11() ext-real real Element of REAL
|.(x - g).| * |.(x - g).| is V11() ext-real non negative real set
|((S1 * (c₆ - x)),(x - g))| is V11() ext-real real Element of REAL
2 * |((S1 * (c₆ - x)),(x - g))| is V11() ext-real real Element of REAL
(|.(x - g).| ^2) + (2 * |((S1 * (c₆ - x)),(x - g))|) is V11() ext-real real Element of REAL
|.(S1 * (c₆ - x)).| is V11() ext-real non negative real Element of REAL
|.(S1 * (c₆ - x)).| ^2 is V11() ext-real real Element of REAL
|.(S1 * (c₆ - x)).| * |.(S1 * (c₆ - x)).| is V11() ext-real non negative real set
((|.(x - g).| ^2) + (2 * |((S1 * (c₆ - x)),(x - g))|)) + (|.(S1 * (c₆ - x)).| ^2) is V11() ext-real real Element of REAL
S1 * |((c₆ - x),(x - g))| is V11() ext-real real Element of REAL
2 * (S1 * |((c₆ - x),(x - g))|) is V11() ext-real real Element of REAL
(|.(x - g).| ^2) + (2 * (S1 * |((c₆ - x),(x - g))|)) is V11() ext-real real Element of REAL
((|.(x - g).| ^2) + (2 * (S1 * |((c₆ - x),(x - g))|))) + (|.(S1 * (c₆ - x)).| ^2) is V11() ext-real real Element of REAL
2 * |((c₆ - x),(x - g))| is V11() ext-real real Element of REAL
- (2 * |((c₆ - x),(x - g))|) is V11() ext-real real Element of REAL
delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2))) is V11() ext-real real Element of REAL
sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))) is V11() ext-real real Element of REAL
(- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2))))) is V11() ext-real real Element of REAL
2 * (Sum (sqr (yo - W))) is V11() ext-real real Element of REAL
((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W)))) is V11() ext-real real Element of REAL
(- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2))))) is V11() ext-real real Element of REAL
((- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W)))) is V11() ext-real real Element of REAL
|.(W - f1).| is V11() ext-real non negative real Element of REAL
sqrt (Sum (sqr (W - f1))) is V11() ext-real real Element of REAL
|.(W - f1).| ^2 is V11() ext-real real Element of REAL
|.(W - f1).| * |.(W - f1).| is V11() ext-real non negative real set
(2 * |((c₆ - x),(x - g))|) ^2 is V11() ext-real real Element of REAL
(2 * |((c₆ - x),(x - g))|) * (2 * |((c₆ - x),(x - g))|) is V11() ext-real non negative real set
4 * (Sum (sqr (yo - W))) is V11() ext-real real Element of REAL
(4 * (Sum (sqr (yo - W)))) * ((Sum (sqr (W - f1))) - (o ^2)) is V11() ext-real real Element of REAL
((2 * |((c₆ - x),(x - g))|) ^2) - ((4 * (Sum (sqr (yo - W)))) * ((Sum (sqr (W - f1))) - (o ^2))) is V11() ext-real real Element of REAL
(sqrt (Sum (sqr (W - f1)))) ^2 is V11() ext-real real Element of REAL
(sqrt (Sum (sqr (W - f1)))) * (sqrt (Sum (sqr (W - f1)))) is V11() ext-real non negative real set
dy is V11() ext-real real set
Polynom ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)),dy) is set
dy ^2 is V11() ext-real real set
dy * dy is V11() ext-real non negative real set
(Sum (sqr (yo - W))) * (dy ^2) is V11() ext-real real Element of REAL
(2 * |((c₆ - x),(x - g))|) * dy is V11() ext-real real Element of REAL
((Sum (sqr (yo - W))) * (dy ^2)) + ((2 * |((c₆ - x),(x - g))|) * dy) is V11() ext-real real Element of REAL
(((Sum (sqr (yo - W))) * (dy ^2)) + ((2 * |((c₆ - x),(x - g))|) * dy)) + ((Sum (sqr (W - f1))) - (o ^2)) is V11() ext-real real Element of REAL
dy - (((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))) is V11() ext-real real Element of REAL
(Sum (sqr (yo - W))) * (dy - (((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W)))))) is V11() ext-real real Element of REAL
dy - (((- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))) is V11() ext-real real Element of REAL
((Sum (sqr (yo - W))) * (dy - (((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))))) * (dy - (((- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W)))))) is V11() ext-real real Element of REAL
(dy - (((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W)))))) * (dy - (((- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W)))))) is V11() ext-real real Element of REAL
(Sum (sqr (yo - W))) * ((dy - (((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W)))))) * (dy - (((- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))))) is V11() ext-real real Element of REAL
Quard ((Sum (sqr (yo - W))),(((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))),(((- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))),dy) is set
((Sum (sqr (W - f1))) - (o ^2)) / (Sum (sqr (yo - W))) is V11() ext-real real Element of REAL
(((- (2 * |((c₆ - x),(x - g))|)) - (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))) * (((- (2 * |((c₆ - x),(x - g))|)) + (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) / (2 * (Sum (sqr (yo - W))))) is V11() ext-real real Element of REAL
- (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2))))) is V11() ext-real real Element of REAL
(- (sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)))))) - (2 * |((c₆ - x),(x - g))|) is V11() ext-real real Element of REAL
(sqrt (delta ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2))))) - (2 * |((c₆ - x),(x - g))|) is V11() ext-real real Element of REAL
4 * ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2)))) is V11() ext-real real Element of REAL
(sqrt 4) * (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2))))) is V11() ext-real real Element of REAL
(- (2 * |((c₆ - x),(x - g))|)) + ((sqrt 4) * (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2)))))) is V11() ext-real real Element of REAL
((- (2 * |((c₆ - x),(x - g))|)) + ((sqrt 4) * (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2))))))) / (2 * (Sum (sqr (yo - W)))) is V11() ext-real real Element of REAL
|((c₆ - x),(x - g))| - (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2))))) is V11() ext-real real Element of REAL
- (|((c₆ - x),(x - g))| - (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2)))))) is V11() ext-real real Element of REAL
2 * (- (|((c₆ - x),(x - g))| - (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2))))))) is V11() ext-real real Element of REAL
(2 * (- (|((c₆ - x),(x - g))| - (sqrt ((|((c₆ - x),(x - g))| ^2) - ((Sum (sqr (yo - W))) * ((Sum (sqr (W - f1))) - (o ^2)))))))) / (2 * (Sum (sqr (yo - W)))) is V11() ext-real real Element of REAL
x + (S1 * c₆) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (S1 * c₆) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x + (S1 * c₆)) - (S1 * x) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),(x + (S1 * c₆)),(- (S1 * x))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(x + (S1 * c₆)) + (- (S1 * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(x + (S1 * c₆)) - (S1 * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(S1 * c₆) - (S1 * x) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
K269((TOP-REAL f),(S1 * c₆),(- (S1 * x))) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
(S1 * c₆) + (- (S1 * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(S1 * c₆) - (S1 * x) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x + ((S1 * c₆) - (S1 * x)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + ((S1 * c₆) - (S1 * x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
x + (S1 * (c₆ - x)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (S1 * (c₆ - x)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
abs S1 is V11() ext-real real Element of REAL
|.(c₆ - x).| is V11() ext-real non negative real Element of REAL
(abs S1) * |.(c₆ - x).| is V11() ext-real real Element of REAL
((abs S1) * |.(c₆ - x).|) ^2 is V11() ext-real real Element of REAL
((abs S1) * |.(c₆ - x).|) * ((abs S1) * |.(c₆ - x).|) is V11() ext-real non negative real set
(abs S1) ^2 is V11() ext-real real Element of REAL
(abs S1) * (abs S1) is V11() ext-real non negative real set
|.(c₆ - x).| ^2 is V11() ext-real real Element of REAL
|.(c₆ - x).| * |.(c₆ - x).| is V11() ext-real non negative real set
((abs S1) ^2) * (|.(c₆ - x).| ^2) is V11() ext-real real Element of REAL
S1 ^2 is V11() ext-real real set
S1 * S1 is V11() ext-real non negative real set
(S1 ^2) * (|.(c₆ - x).| ^2) is V11() ext-real real Element of REAL
(Sum (sqr (yo - W))) * (S1 ^2) is V11() ext-real real Element of REAL
(2 * |((c₆ - x),(x - g))|) * S1 is V11() ext-real real Element of REAL
((Sum (sqr (yo - W))) * (S1 ^2)) + ((2 * |((c₆ - x),(x - g))|) * S1) is V11() ext-real real Element of REAL
(((Sum (sqr (yo - W))) * (S1 ^2)) + ((2 * |((c₆ - x),(x - g))|) * S1)) + ((Sum (sqr (W - f1))) - (o ^2)) is V11() ext-real real Element of REAL
|.(yo - W).| ^2 is V11() ext-real real Element of REAL
|.(yo - W).| * |.(yo - W).| is V11() ext-real non negative real set
(|.(yo - W).| ^2) * (S1 ^2) is V11() ext-real real Element of REAL
((|.(yo - W).| ^2) * (S1 ^2)) + ((2 * |((c₆ - x),(x - g))|) * S1) is V11() ext-real real Element of REAL
(|.(W - f1).| ^2) - (o ^2) is V11() ext-real real Element of REAL
(((|.(yo - W).| ^2) * (S1 ^2)) + ((2 * |((c₆ - x),(x - g))|) * S1)) + ((|.(W - f1).| ^2) - (o ^2)) is V11() ext-real real Element of REAL
(|.(c₆ - x).| ^2) * (S1 ^2) is V11() ext-real real Element of REAL
((|.(c₆ - x).| ^2) * (S1 ^2)) + ((2 * |((c₆ - x),(x - g))|) * S1) is V11() ext-real real Element of REAL
(|.(x - g).| ^2) - (o ^2) is V11() ext-real real Element of REAL
(((|.(c₆ - x).| ^2) * (S1 ^2)) + ((2 * |((c₆ - x),(x - g))|) * S1)) + ((|.(x - g).| ^2) - (o ^2)) is V11() ext-real real Element of REAL
Polynom ((Sum (sqr (yo - W))),(2 * |((c₆ - x),(x - g))|),((Sum (sqr (W - f1))) - (o ^2)),S1) is set
0. (TOP-REAL f) is V16() Function-like V50(f) V51() V68( TOP-REAL f) complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
the ZeroF of (TOP-REAL f) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (0. (TOP-REAL f)) is V16() Function-like V50(f) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL f)
x + (0. (TOP-REAL f)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(- (2 * |((c₆ - x),(x - g))|)) - (2 * |((c₆ - x),(x - g))|) is V11() ext-real real Element of REAL
((- (2 * |((c₆ - x),(x - g))|)) - (2 * |((c₆ - x),(x - g))|)) / (2 * (Sum (sqr (yo - W)))) is V11() ext-real real Element of REAL
(- (2 * |((c₆ - x),(x - g))|)) - (- (2 * |((c₆ - x),(x - g))|)) is V11() ext-real real Element of REAL
((- (2 * |((c₆ - x),(x - g))|)) - (- (2 * |((c₆ - x),(x - g))|))) / (2 * (Sum (sqr (yo - W)))) is V11() ext-real real Element of REAL
r is V11() ext-real real set
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 V11() ext-real real set
x is V11() ext-real real set
c₆ is V11() ext-real real set
g is V11() ext-real real set
c₆ * f is V11() ext-real real set
g * x is V11() ext-real real set
(c₆ * f) + (g * x) is V11() ext-real real set
- ((c₆ * f) + (g * x)) is V11() ext-real real set
((c₆ * f) + (g * x)) ^2 is V11() ext-real real set
((c₆ * f) + (g * x)) * ((c₆ * f) + (g * x)) is V11() ext-real non negative real set
f ^2 is V11() ext-real real set
f * f is V11() ext-real non negative real set
x ^2 is V11() ext-real real set
x * x is V11() ext-real non negative real set
(f ^2) + (x ^2) is V11() ext-real real set
c₆ ^2 is V11() ext-real real set
c₆ * c₆ is V11() ext-real non negative real set
g ^2 is V11() ext-real real set
g * g is V11() ext-real non negative real set
(c₆ ^2) + (g ^2) is V11() ext-real real set
((c₆ ^2) + (g ^2)) - (o ^2) is V11() ext-real real set
((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2)) is V11() ext-real real set
(((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2))) is V11() ext-real real set
sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2)))) is V11() ext-real real set
(- ((c₆ * f) + (g * x))) + (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real set
((- ((c₆ * f) + (g * x))) + (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2)))))) / ((f ^2) + (x ^2)) is V11() ext-real real set
r * f is V11() ext-real real set
r * x is V11() ext-real real set
W is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
f1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(2,f1,o) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL 2
cl_Ball (f1,o) is non empty closed V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (cl_Ball (f1,o)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of (2,f1,o) is non empty set
yo is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
yo `1 is V11() ext-real real Element of REAL
W `1 is V11() ext-real real Element of REAL
(yo `1) - (W `1) is V11() ext-real real Element of REAL
yo `2 is V11() ext-real real Element of REAL
W `2 is V11() ext-real real Element of REAL
(yo `2) - (W `2) is V11() ext-real real Element of REAL
f1 `1 is V11() ext-real real Element of REAL
(W `1) - (f1 `1) is V11() ext-real real Element of REAL
f1 `2 is V11() ext-real real Element of REAL
(W `2) - (f1 `2) is V11() ext-real real Element of REAL
(2,f1,W,yo,o) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(W `1) + (r * f) is V11() ext-real real Element of REAL
(W `2) + (r * x) is V11() ext-real real Element of REAL
|[((W `1) + (r * f)),((W `2) + (r * x))]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W - f1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- f1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- f1 is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL 2),W,(- f1)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W + (- f1) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
W - f1 is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.(W - f1).| is V11() ext-real non negative real Element of REAL
|.(W - f1).| ^2 is V11() ext-real real Element of REAL
|.(W - f1).| * |.(W - f1).| is V11() ext-real non negative real set
2 * ((c₆ * f) + (g * x)) is V11() ext-real real Element of REAL
- (2 * ((c₆ * f) + (g * x))) is V11() ext-real real Element of REAL
delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))) is V11() ext-real real set
sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))) is V11() ext-real real set
(- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real Element of REAL
2 * ((f ^2) + (x ^2)) is V11() ext-real real Element of REAL
((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2))) is V11() ext-real real Element of REAL
(- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real Element of REAL
((- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2))) is V11() ext-real real Element of REAL
(2 * ((c₆ * f) + (g * x))) ^2 is V11() ext-real real Element of REAL
(2 * ((c₆ * f) + (g * x))) * (2 * ((c₆ * f) + (g * x))) is V11() ext-real non negative real set
4 * ((f ^2) + (x ^2)) is V11() ext-real real Element of REAL
(4 * ((f ^2) + (x ^2))) * (((c₆ ^2) + (g ^2)) - (o ^2)) is V11() ext-real real Element of REAL
((2 * ((c₆ * f) + (g * x))) ^2) - ((4 * ((f ^2) + (x ^2))) * (((c₆ ^2) + (g ^2)) - (o ^2))) is V11() ext-real real Element of REAL
(W - f1) `1 is V11() ext-real real Element of REAL
((W - f1) `1) ^2 is V11() ext-real real Element of REAL
((W - f1) `1) * ((W - f1) `1) is V11() ext-real non negative real set
(W - f1) `2 is V11() ext-real real Element of REAL
((W - f1) `2) ^2 is V11() ext-real real Element of REAL
((W - f1) `2) * ((W - f1) `2) is V11() ext-real non negative real set
(((W - f1) `1) ^2) + (((W - f1) `2) ^2) is V11() ext-real real Element of REAL
(c₆ ^2) + (((W - f1) `2) ^2) is V11() ext-real real Element of REAL
(o ^2) - (o ^2) is V11() ext-real real set
- (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real set
(- (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) - (2 * ((c₆ * f) + (g * x))) is V11() ext-real real Element of REAL
(sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))))) - (2 * ((c₆ * f) + (g * x))) is V11() ext-real real Element of REAL
(- (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real set
(sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real set
0 + 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 complex-yielding V131() V132() V133() V134() V135() V136() V137() V140() V141() V142() V143() V144() V145() V146() set
TD is V11() ext-real real set
Polynom (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)),TD) is set
Quard (((f ^2) + (x ^2)),(((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))),(((- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))),TD) is set
TD ^2 is V11() ext-real real set
TD * TD is V11() ext-real non negative real set
((f ^2) + (x ^2)) * (TD ^2) is V11() ext-real real set
(2 * ((c₆ * f) + (g * x))) * TD is V11() ext-real real Element of REAL
(((f ^2) + (x ^2)) * (TD ^2)) + ((2 * ((c₆ * f) + (g * x))) * TD) is V11() ext-real real Element of REAL
((((f ^2) + (x ^2)) * (TD ^2)) + ((2 * ((c₆ * f) + (g * x))) * TD)) + (((c₆ ^2) + (g ^2)) - (o ^2)) is V11() ext-real real Element of REAL
TD - (((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))) is V11() ext-real real Element of REAL
((f ^2) + (x ^2)) * (TD - (((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2))))) is V11() ext-real real Element of REAL
TD - (((- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))) is V11() ext-real real Element of REAL
(((f ^2) + (x ^2)) * (TD - (((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))))) * (TD - (((- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2))))) is V11() ext-real real Element of REAL
(TD - (((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2))))) * (TD - (((- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2))))) is V11() ext-real real Element of REAL
((f ^2) + (x ^2)) * ((TD - (((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2))))) * (TD - (((- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))))) is V11() ext-real real Element of REAL
(((c₆ ^2) + (g ^2)) - (o ^2)) / ((f ^2) + (x ^2)) is V11() ext-real real set
(((- (2 * ((c₆ * f) + (g * x)))) - (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))) * (((- (2 * ((c₆ * f) + (g * x)))) + (sqrt (delta (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)))))) / (2 * ((f ^2) + (x ^2)))) is V11() ext-real real Element of REAL
4 * ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2)))) is V11() ext-real real Element of REAL
(sqrt 4) * (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real Element of REAL
(- (2 * ((c₆ * f) + (g * x)))) + ((sqrt 4) * (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2)))))) is V11() ext-real real Element of REAL
((- (2 * ((c₆ * f) + (g * x)))) + ((sqrt 4) * (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2))))))) / (2 * ((f ^2) + (x ^2))) is V11() ext-real real Element of REAL
((c₆ * f) + (g * x)) - (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2))))) is V11() ext-real real set
- (((c₆ * f) + (g * x)) - (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2)))))) is V11() ext-real real set
2 * (- (((c₆ * f) + (g * x)) - (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2))))))) is V11() ext-real real Element of REAL
(2 * (- (((c₆ * f) + (g * x)) - (sqrt ((((c₆ * f) + (g * x)) ^2) - (((f ^2) + (x ^2)) * (((c₆ ^2) + (g ^2)) - (o ^2)))))))) / (2 * ((f ^2) + (x ^2))) is V11() ext-real real Element of REAL
halfline (W,yo) is non empty convex Element of bool the carrier of (TOP-REAL 2)
Sphere (f1,o) is non empty closed V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(halfline (W,yo)) /\ (Sphere (f1,o)) is Element of bool the carrier of (TOP-REAL 2)
f is V11() ext-real real set
1 - f is V11() ext-real real Element of REAL
(1 - f) * W is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
the U10 of (TOP-REAL 2) is non empty V16() V19([:REAL, the carrier of (TOP-REAL 2):]) V20( the carrier of (TOP-REAL 2)) Function-like total quasi_total Element of bool [:[:REAL, the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[:REAL, the carrier of (TOP-REAL 2):] is non empty V16() set
[:[:REAL, the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty V16() set
bool [:[:REAL, the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty set
the U10 of (TOP-REAL 2) . ((1 - f),W) is set
[(1 - f),W] is non empty set
{(1 - f),W} is non empty set
{(1 - f)} is non empty trivial V140() V141() V142() set
{{(1 - f),W},{(1 - f)}} is non empty set
the U10 of (TOP-REAL 2) . [(1 - f),W] is set
(1 - f) * W is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
f * yo is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
the U10 of (TOP-REAL 2) . (f,yo) is set
[f,yo] is non empty set
{f,yo} is non empty set
{f} is non empty trivial V140() V141() V142() set
{{f,yo},{f}} is non empty set
the U10 of (TOP-REAL 2) . [f,yo] is set
f * yo is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 - f) * W) + (f * yo) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
((1 - f) * W) + (f * yo) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
1 * W is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
the U10 of (TOP-REAL 2) . (1,W) is set
[1,W] is non empty set
{1,W} is non empty set
{1} is non empty trivial V140() V141() V142() V143() V144() V145() set
{{1,W},{1}} is non empty set
the U10 of (TOP-REAL 2) . [1,W] is set
1 * W is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
f * W is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
the U10 of (TOP-REAL 2) . (f,W) is set
[f,W] is non empty set
{f,W} is non empty set
{{f,W},{f}} is non empty set
the U10 of (TOP-REAL 2) . [f,W] is set
f * W is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(1 * W) - (f * W) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- (f * W) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- (f * W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL 2),(1 * W),(- (f * W))) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(1 * W) + (- (f * W)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(1 * W) - (f * W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
((1 * W) - (f * W)) + (f * yo) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
((1 * W) - (f * W)) + (f * yo) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
W - (f * W) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
K269((TOP-REAL 2),W,(- (f * W))) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W + (- (f * W)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
W - (f * W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(W - (f * W)) + (f * yo) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(W - (f * W)) + (f * yo) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
W + (f * yo) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W + (f * yo) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(W + (f * yo)) - (f * W) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
K269((TOP-REAL 2),(W + (f * yo)),(- (f * W))) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(W + (f * yo)) + (- (f * W)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(W + (f * yo)) - (f * W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(f * yo) - (f * W) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
K269((TOP-REAL 2),(f * yo),(- (f * W))) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(f * yo) + (- (f * W)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(f * yo) - (f * W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
W + ((f * yo) - (f * W)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W + ((f * yo) - (f * W)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
yo - W is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- W is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- W is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL 2),yo,(- W)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
yo + (- W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
yo - W is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
f * (yo - W) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
the U10 of (TOP-REAL 2) . (f,(yo - W)) is set
[f,(yo - W)] is non empty set
{f,(yo - W)} is non empty set
{{f,(yo - W)},{f}} is non empty set
the U10 of (TOP-REAL 2) . [f,(yo - W)] is set
f * (yo - W) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
W + (f * (yo - W)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W + (f * (yo - W)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(2,f1,W,yo,o) `1 is V11() ext-real real Element of REAL
(f * (yo - W)) `1 is V11() ext-real real Element of REAL
(W `1) + ((f * (yo - W)) `1) is V11() ext-real real Element of REAL
(yo - W) `1 is V11() ext-real real Element of REAL
f * ((yo - W) `1) is V11() ext-real real Element of REAL
(W `1) + (f * ((yo - W) `1)) is V11() ext-real real Element of REAL
f * ((yo `1) - (W `1)) is V11() ext-real real Element of REAL
(W `1) + (f * ((yo `1) - (W `1))) is V11() ext-real real Element of REAL
(2,f1,W,yo,o) - f1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
K269((TOP-REAL 2),(2,f1,W,yo,o),(- f1)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(2,f1,W,yo,o) + (- f1) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(2,f1,W,yo,o) - f1 is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.((2,f1,W,yo,o) - f1).| is V11() ext-real non negative real Element of REAL
((2,f1,W,yo,o) - f1) `1 is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) - f1) `1) ^2 is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) - f1) `1) * (((2,f1,W,yo,o) - f1) `1) is V11() ext-real non negative real set
((2,f1,W,yo,o) - f1) `2 is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) - f1) `2) ^2 is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) - f1) `2) * (((2,f1,W,yo,o) - f1) `2) is V11() ext-real non negative real set
((((2,f1,W,yo,o) - f1) `1) ^2) + ((((2,f1,W,yo,o) - f1) `2) ^2) is V11() ext-real real Element of REAL
((2,f1,W,yo,o) `1) - (f1 `1) is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) `1) - (f1 `1)) ^2 is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) `1) - (f1 `1)) * (((2,f1,W,yo,o) `1) - (f1 `1)) is V11() ext-real non negative real set
((((2,f1,W,yo,o) `1) - (f1 `1)) ^2) + ((((2,f1,W,yo,o) - f1) `2) ^2) is V11() ext-real real Element of REAL
(2,f1,W,yo,o) `2 is V11() ext-real real Element of REAL
((2,f1,W,yo,o) `2) - (f1 `2) is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) `2) - (f1 `2)) ^2 is V11() ext-real real Element of REAL
(((2,f1,W,yo,o) `2) - (f1 `2)) * (((2,f1,W,yo,o) `2) - (f1 `2)) is V11() ext-real non negative real set
((((2,f1,W,yo,o) `1) - (f1 `1)) ^2) + ((((2,f1,W,yo,o) `2) - (f1 `2)) ^2) is V11() ext-real real Element of REAL
(1 - f) * (W `1) is V11() ext-real real Element of REAL
f * (yo `1) is V11() ext-real real Element of REAL
((1 - f) * (W `1)) + (f * (yo `1)) is V11() ext-real real Element of REAL
(((1 - f) * (W `1)) + (f * (yo `1))) - (f1 `1) is V11() ext-real real Element of REAL
((((1 - f) * (W `1)) + (f * (yo `1))) - (f1 `1)) ^2 is V11() ext-real real Element of REAL
((((1 - f) * (W `1)) + (f * (yo `1))) - (f1 `1)) * ((((1 - f) * (W `1)) + (f * (yo `1))) - (f1 `1)) is V11() ext-real non negative real set
(((((1 - f) * (W `1)) + (f * (yo `1))) - (f1 `1)) ^2) + ((((2,f1,W,yo,o) `2) - (f1 `2)) ^2) is V11() ext-real real Element of REAL
(1 - f) * (W `2) is V11() ext-real real Element of REAL
f * (yo `2) is V11() ext-real real Element of REAL
((1 - f) * (W `2)) + (f * (yo `2)) is V11() ext-real real Element of REAL
(((1 - f) * (W `2)) + (f * (yo `2))) - (f1 `2) is V11() ext-real real Element of REAL
((((1 - f) * (W `2)) + (f * (yo `2))) - (f1 `2)) ^2 is V11() ext-real real Element of REAL
((((1 - f) * (W `2)) + (f * (yo `2))) - (f1 `2)) * ((((1 - f) * (W `2)) + (f * (yo `2))) - (f1 `2)) is V11() ext-real non negative real set
(((((1 - f) * (W `1)) + (f * (yo `1))) - (f1 `1)) ^2) + (((((1 - f) * (W `2)) + (f * (yo `2))) - (f1 `2)) ^2) is V11() ext-real real Element of REAL
f ^2 is V11() ext-real real set
f * f is V11() ext-real non negative real set
(f ^2) * ((f ^2) + (x ^2)) is V11() ext-real real set
f * 2 is V11() ext-real real Element of REAL
(f * 2) * ((c₆ * f) + (g * x)) is V11() ext-real real Element of REAL
((f ^2) * ((f ^2) + (x ^2))) + ((f * 2) * ((c₆ * f) + (g * x))) is V11() ext-real real Element of REAL
(((f ^2) * ((f ^2) + (x ^2))) + ((f * 2) * ((c₆ * f) + (g * x)))) + (c₆ ^2) is V11() ext-real real Element of REAL
((((f ^2) * ((f ^2) + (x ^2))) + ((f * 2) * ((c₆ * f) + (g * x)))) + (c₆ ^2)) + (g ^2) is V11() ext-real real Element of REAL
((f ^2) + (x ^2)) * (f ^2) is V11() ext-real real set
(2 * ((c₆ * f) + (g * x))) * f is V11() ext-real real Element of REAL
(((f ^2) + (x ^2)) * (f ^2)) + ((2 * ((c₆ * f) + (g * x))) * f) is V11() ext-real real Element of REAL
((((f ^2) + (x ^2)) * (f ^2)) + ((2 * ((c₆ * f) + (g * x))) * f)) + (((c₆ ^2) + (g ^2)) - (o ^2)) is V11() ext-real real Element of REAL
Polynom (((f ^2) + (x ^2)),(2 * ((c₆ * f) + (g * x))),(((c₆ ^2) + (g ^2)) - (o ^2)),f) is set
(f * (yo - W)) `2 is V11() ext-real real Element of REAL
(W `2) + ((f * (yo - W)) `2) is V11() ext-real real Element of REAL
(yo - W) `2 is V11() ext-real real Element of REAL
f * ((yo - W) `2) is V11() ext-real real Element of REAL
(W `2) + (f * ((yo - W) `2)) is V11() ext-real real Element of REAL
f * ((yo `2) - (W `2)) is V11() ext-real real Element of REAL
(W `2) + (f * ((yo `2) - (W `2))) is V11() ext-real real Element of REAL
0. (TOP-REAL 2) is V16() Function-like V50(2) V51() V68( TOP-REAL 2) complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W + (0. (TOP-REAL 2)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W + (0. (TOP-REAL 2)) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
(- (2 * ((c₆ * f) + (g * x)))) - (2 * ((c₆ * f) + (g * x))) is V11() ext-real real Element of REAL
((- (2 * ((c₆ * f) + (g * x)))) - (2 * ((c₆ * f) + (g * x)))) / (2 * ((f ^2) + (x ^2))) is V11() ext-real real Element of REAL
(- (2 * ((c₆ * f) + (g * x)))) - (- (2 * ((c₆ * f) + (g * x)))) is V11() ext-real real Element of REAL
((- (2 * ((c₆ * f) + (g * x)))) - (- (2 * ((c₆ * f) + (g * x))))) / (2 * ((f ^2) + (x ^2))) is V11() ext-real real Element of REAL
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
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 non empty TopSpace-like pathwise_connected convex 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
the carrier of (r,o,f) is non empty set
[: the carrier of (r,o,f), the carrier of (r,o,f):] is non empty V16() set
bool [: the carrier of (r,o,f), the carrier of (r,o,f):] is non empty set
x is Element of the carrier of (r,o,f)
c₆ is non empty V16() V19( the carrier of (r,o,f)) V20( the carrier of (r,o,f)) Function-like total quasi_total Element of bool [: the carrier of (r,o,f), the carrier of (r,o,f):]
Tcircle (o,f) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (o,f)) is non empty set
c₆ . x is Element of the carrier of (r,o,f)
W is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
g is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
(r,o,W,g,f) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
yo is Element of the carrier of (Tcircle (o,f))
yo is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
f1 is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
g is Element of the carrier of (Tcircle (o,f))
(r,o,f1,yo,f) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
D2 is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
S1 is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
W is Element of the carrier of (Tcircle (o,f))
(r,o,S1,D2,f) is V16() Function-like V50(r) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL r)
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)
(o,f,r) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL o
cl_Ball (f,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 (f,r)) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (o,f,r) is non empty set
[: the carrier of (o,f,r), the carrier of (o,f,r):] is non empty V16() set
bool [: the carrier of (o,f,r), the carrier of (o,f,r):] is non empty set
Tcircle (f,r) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (Tcircle (f,r)) is non empty set
x is Element of the carrier of (o,f,r)
c₆ is non empty V16() V19( the carrier of (o,f,r)) V20( the carrier of (o,f,r)) Function-like total quasi_total Element of bool [: the carrier of (o,f,r), the carrier of (o,f,r):]
(o,f,r,x,c₆) is Element of the carrier of (Tcircle (f,r))
c₆ . x is Element of the carrier of (o,f,r)
Sphere (f,r) is non empty closed V217( TOP-REAL o) Element of bool the carrier of (TOP-REAL o)
g is V16() Function-like V50(o) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL o)
W is V16() Function-like V50(o) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL o)
(o,f,W,g,r) is V16() Function-like V50(o) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL o)
halfline (W,g) is non empty convex Element of bool the carrier of (TOP-REAL o)
(halfline (W,g)) /\ (Sphere (f,r)) is Element of bool the carrier of (TOP-REAL o)
r is non empty V11() ext-real positive non negative real set
o is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(2,o,r) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL 2
cl_Ball (o,r) is non empty closed V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (cl_Ball (o,r)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
Tcircle (o,r) is non empty strict TopSpace-like pathwise_connected V236() SubSpace of TOP-REAL 2
f is non empty TopSpace-like SubSpace of (2,o,r)
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
the carrier of (Tcircle (o,r)) is non empty set
Sphere (o,r) is non empty closed V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
the carrier of (2,o,r) is non empty set
g is Element of the carrier of (2,o,r)
the non empty V16() V19( the carrier of K582()) V20( the carrier of (2,o,r)) Function-like constant total quasi_total continuous M28((2,o,r),g,g) is non empty V16() V19( the carrier of K582()) V20( the carrier of (2,o,r)) Function-like constant total quasi_total continuous M28((2,o,r),g,g)
I[01] --> g is non empty V16() V19( the carrier of I[01]) V20( the carrier of (2,o,r)) Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (2,o,r):]
[: the carrier of I[01], the carrier of (2,o,r):] is non empty V16() set
bool [: the carrier of I[01], the carrier of (2,o,r):] is non empty set
the carrier of I[01] --> g is non empty V16() V19( the carrier of I[01]) V20( the carrier of (2,o,r)) Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of (2,o,r):]
the carrier of I[01] --> the Element of the carrier of f is non empty V16() V19( the carrier of I[01]) V20( the carrier of f) Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of f:]
[: the carrier of I[01], the carrier of f:] is non empty V16() set
bool [: the carrier of I[01], the carrier of f:] is non empty set
D2 is non empty V16() V19( the carrier of I[01]) V20( the carrier of f) Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of f:]
I[01] --> the Element of the carrier of f is non empty V16() V19( the carrier of I[01]) V20( the carrier of f) Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of f:]
W is V11() ext-real real Element of the carrier of I[01]
D2 . W is Element of the carrier of f
yo is V11() ext-real real Element of the carrier of I[01]
D2 . yo is Element of the carrier of f
[: the carrier of (2,o,r), the carrier of f:] is non empty V16() set
bool [: the carrier of (2,o,r), the carrier of f:] is non empty set
OK is non empty V16() V19( the carrier of (2,o,r)) V20( the carrier of f) Function-like total quasi_total continuous Element of bool [: the carrier of (2,o,r), the carrier of f:]
FundamentalGroup (f, the Element of the carrier of f) is non empty V89() V111() V112() V113() V162() V163() V164() V165() V166() V167() L8()
the carrier of (FundamentalGroup (f, the Element of the carrier of f)) is non empty set
Loops the Element of the carrier of f is non empty set
Paths ( the Element of the carrier of f, the Element of the carrier of f) is non empty set
EqRel (f, the Element of the carrier of f) is non empty V16() V19( Loops the Element of the carrier of f) V20( Loops the Element of the carrier of f) total quasi_total V37() V42() Element of bool [:(Loops the Element of the carrier of f),(Loops the Element of the carrier of f):]
[:(Loops the Element of the carrier of f),(Loops the Element of the carrier of f):] is non empty V16() set
bool [:(Loops the Element of the carrier of f),(Loops the Element of the carrier of f):] is non empty set
EqRel (f, the Element of the carrier of f, the Element of the carrier of f) is V16() V19( Paths ( the Element of the carrier of f, the Element of the carrier of f)) V20( Paths ( the Element of the carrier of f, the Element of the carrier of f)) Element of bool [:(Paths ( the Element of the carrier of f, the Element of the carrier of f)),(Paths ( the Element of the carrier of f, the Element of the carrier of f)):]
[:(Paths ( the Element of the carrier of f, the Element of the carrier of f)),(Paths ( the Element of the carrier of f, the Element of the carrier of f)):] is non empty V16() set
bool [:(Paths ( the Element of the carrier of f, the Element of the carrier of f)),(Paths ( the Element of the carrier of f, the Element of the carrier of f)):] is non empty set
S1 is non empty V16() V19( the carrier of K582()) V20( the carrier of f) Function-like constant total quasi_total M28(f, the Element of the carrier of f, the Element of the carrier of f)
Class ((EqRel (f, the Element of the carrier of f)),S1) is Element of bool (Loops the Element of the carrier of f)
bool (Loops the Element of the carrier of f) is non empty set
{(Class ((EqRel (f, the Element of the carrier of f)),S1))} is non empty trivial set
OK is set
Zf1 is non empty V16() V19( the carrier of K582()) V20( the carrier of f) Function-like total quasi_total M28(f, the Element of the carrier of f, the Element of the carrier of f)
Class ((EqRel (f, the Element of the carrier of f)),Zf1) is Element of bool (Loops the Element of the carrier of f)
TD is non empty V16() V19( the carrier of K582()) V20( the carrier of (2,o,r)) Function-like total quasi_total continuous M28((2,o,r),g,g)
[: the carrier of [:I[01],I[01]:], the carrier of (2,o,r):] is non empty V16() set
bool [: the carrier of [:I[01],I[01]:], the carrier of (2,o,r):] is non empty set
f is non empty V16() V19( the carrier of [:I[01],I[01]:]) V20( the carrier of (2,o,r)) Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (2,o,r):]
[: the carrier of [:I[01],I[01]:], the carrier of f:] is non empty V16() set
bool [: the carrier of [:I[01],I[01]:], the carrier of f:] is non empty set
OK * f is non empty V16() V19( the carrier of [:I[01],I[01]:]) V20( the carrier of f) Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of f:]
dy is non empty V16() V19( the carrier of [:I[01],I[01]:]) V20( the carrier of f) Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of f:]
fy2 is V11() ext-real real Element of the carrier of I[01]
dy . (fy2,0) is set
[fy2,0] is non empty set
{fy2,0} is non empty V140() V141() V142() set
{fy2} is non empty trivial V140() V141() V142() set
{{fy2,0},{fy2}} is non empty set
dy . [fy2,0] is set
Zf1 . fy2 is Element of the carrier of f
dy . (fy2,1) is set
[fy2,1] is non empty set
{fy2,1} is non empty V140() V141() V142() set
{{fy2,1},{fy2}} is non empty set
dy . [fy2,1] is set
S1 . fy2 is Element of the carrier of f
dy . (0,fy2) is set
[0,fy2] is non empty set
{0,fy2} is non empty V140() V141() V142() set
{{0,fy2},{0}} is non empty set
dy . [0,fy2] is set
dy . (1,fy2) is set
[1,fy2] is non empty set
{1,fy2} is non empty V140() V141() V142() set
{1} is non empty trivial V140() V141() V142() V143() V144() V145() set
{{1,fy2},{1}} is non empty set
dy . [1,fy2] is set
[fy2,W] is non empty Element of the carrier of [:I[01],I[01]:]
{fy2,W} is non empty V140() V141() V142() set
{{fy2,W},{fy2}} is non empty set
dy . [fy2,W] is Element of the carrier of f
f . (fy2,0) is set
f . [fy2,0] is set
OK . (f . (fy2,0)) is set
TD . fy2 is Element of the carrier of (2,o,r)
OK . (TD . fy2) is Element of the carrier of f
Zf1 . fy2 is Element of the carrier of f
[fy2,yo] is non empty Element of the carrier of [:I[01],I[01]:]
{fy2,yo} is non empty V140() V141() V142() set
{{fy2,yo},{fy2}} is non empty set
dy . [fy2,yo] is Element of the carrier of f
f . (fy2,1) is set
f . [fy2,1] is set
OK . (f . (fy2,1)) is set
the non empty V16() V19( the carrier of K582()) V20( the carrier of (2,o,r)) Function-like constant total quasi_total continuous M28((2,o,r),g,g) . fy2 is Element of the carrier of (2,o,r)
OK . ( the non empty V16() V19( the carrier of K582()) V20( the carrier of (2,o,r)) Function-like constant total quasi_total continuous M28((2,o,r),g,g) . fy2) is Element of the carrier of f
S1 . fy2 is Element of the carrier of f
[W,fy2] is non empty Element of the carrier of [:I[01],I[01]:]
{W,fy2} is non empty V140() V141() V142() set
{W} is non empty trivial V140() V141() V142() set
{{W,fy2},{W}} is non empty set
dy . [W,fy2] is Element of the carrier of f
f . (0,fy2) is set
f . [0,fy2] is set
OK . (f . (0,fy2)) is set
OK . g is Element of the carrier of f
[yo,fy2] is non empty Element of the carrier of [:I[01],I[01]:]
{yo,fy2} is non empty V140() V141() V142() set
{yo} is non empty trivial V140() V141() V142() set
{{yo,fy2},{yo}} is non empty set
dy . [yo,fy2] is Element of the carrier of f
f . (1,fy2) is set
f . [1,fy2] is set
OK . (f . (1,fy2)) is set
OK is set
Class (EqRel (f, the Element of the carrier of f)) is a_partition of Loops the Element of the carrier of f
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 V11() ext-real non negative real set
(r,f,o) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL r
cl_Ball (f,o) 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 (f,o)) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (r,f,o) is non empty set
[: the carrier of (r,f,o), the carrier of (r,f,o):] is non empty V16() set
bool [: the carrier of (r,f,o), the carrier of (r,f,o):] is non empty set
Tcircle (f,o) is non empty strict TopSpace-like SubSpace of TOP-REAL r
the carrier of (Tcircle (f,o)) is non empty set
[: the carrier of (r,f,o), the carrier of (Tcircle (f,o)):] is non empty V16() set
bool [: the carrier of (r,f,o), the carrier of (Tcircle (f,o)):] is non empty set
x is non empty V16() V19( the carrier of (r,f,o)) V20( the carrier of (r,f,o)) Function-like total quasi_total Element of bool [: the carrier of (r,f,o), the carrier of (r,f,o):]
c₆ is Element of the carrier of (r,f,o)
(r,f,o,c₆,x) is Element of the carrier of (Tcircle (f,o))
c₆ is non empty V16() V19( the carrier of (r,f,o)) V20( the carrier of (Tcircle (f,o))) Function-like total quasi_total Element of bool [: the carrier of (r,f,o), the carrier of (Tcircle (f,o)):]
c₆ is non empty V16() V19( the carrier of (r,f,o)) V20( the carrier of (Tcircle (f,o))) Function-like total quasi_total Element of bool [: the carrier of (r,f,o), the carrier of (Tcircle (f,o)):]
g is non empty V16() V19( the carrier of (r,f,o)) V20( the carrier of (Tcircle (f,o))) Function-like total quasi_total Element of bool [: the carrier of (r,f,o), the carrier of (Tcircle (f,o)):]
W is Element of the carrier of (r,f,o)
c₆ . W is Element of the carrier of (Tcircle (f,o))
g . W is Element of the carrier of (Tcircle (f,o))
(r,f,o,W,x) is Element of the carrier of (Tcircle (f,o))
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)
(o,f,r) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL o
cl_Ball (f,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 (f,r)) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (o,f,r) is non empty set
[: the carrier of (o,f,r), the carrier of (o,f,r):] is non empty V16() set
bool [: the carrier of (o,f,r), the carrier of (o,f,r):] is non empty set
Tcircle (f,r) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (Tcircle (f,r)) is non empty set
x is Element of the carrier of (o,f,r)
c₆ is non empty V16() V19( the carrier of (o,f,r)) V20( the carrier of (o,f,r)) Function-like total quasi_total Element of bool [: the carrier of (o,f,r), the carrier of (o,f,r):]
(o,r,f,c₆) is non empty V16() V19( the carrier of (o,f,r)) V20( the carrier of (Tcircle (f,r))) Function-like total quasi_total Element of bool [: the carrier of (o,f,r), the carrier of (Tcircle (f,r)):]
[: the carrier of (o,f,r), the carrier of (Tcircle (f,r)):] is non empty V16() set
bool [: the carrier of (o,f,r), the carrier of (Tcircle (f,r)):] is non empty set
(o,r,f,c₆) . x is Element of the carrier of (Tcircle (f,r))
(o,f,r,x,c₆) is Element of the carrier of (Tcircle (f,r))
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)
(o,f,r) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL o
cl_Ball (f,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 (f,r)) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (o,f,r) is non empty set
[: the carrier of (o,f,r), the carrier of (o,f,r):] is non empty V16() set
bool [: the carrier of (o,f,r), the carrier of (o,f,r):] is non empty set
Tcircle (f,r) is non empty strict TopSpace-like SubSpace of TOP-REAL o
the carrier of (Tcircle (f,r)) is non empty set
Sphere (f,r) is non empty closed V217( TOP-REAL o) Element of bool the carrier of (TOP-REAL o)
id (Tcircle (f,r)) is non empty V16() V19( the carrier of (Tcircle (f,r))) V20( the carrier of (Tcircle (f,r))) Function-like total quasi_total Element of bool [: the carrier of (Tcircle (f,r)), the carrier of (Tcircle (f,r)):]
[: the carrier of (Tcircle (f,r)), the carrier of (Tcircle (f,r)):] is non empty V16() set
bool [: the carrier of (Tcircle (f,r)), the carrier of (Tcircle (f,r)):] is non empty set
id the carrier of (Tcircle (f,r)) is non empty V16() V19( the carrier of (Tcircle (f,r))) V20( the carrier of (Tcircle (f,r))) Function-like one-to-one total quasi_total Element of bool [: the carrier of (Tcircle (f,r)), the carrier of (Tcircle (f,r)):]
x is non empty V16() V19( the carrier of (o,f,r)) V20( the carrier of (o,f,r)) Function-like total quasi_total continuous Element of bool [: the carrier of (o,f,r), the carrier of (o,f,r):]
(o,r,f,x) is non empty V16() V19( the carrier of (o,f,r)) V20( the carrier of (Tcircle (f,r))) Function-like total quasi_total Element of bool [: the carrier of (o,f,r), the carrier of (Tcircle (f,r)):]
[: the carrier of (o,f,r), the carrier of (Tcircle (f,r)):] is non empty V16() set
bool [: the carrier of (o,f,r), the carrier of (Tcircle (f,r)):] is non empty set
(o,r,f,x) | (Sphere (f,r)) is V16() V19( the carrier of (o,f,r)) V19( Sphere (f,r)) V19( the carrier of (o,f,r)) V20( the carrier of (Tcircle (f,r))) Function-like Element of bool [: the carrier of (o,f,r), the carrier of (Tcircle (f,r)):]
dom (o,r,f,x) is non empty Element of bool the carrier of (o,f,r)
bool the carrier of (o,f,r) is non empty set
dom ((o,r,f,x) | (Sphere (f,r))) is Element of bool (Sphere (f,r))
bool (Sphere (f,r)) is non empty set
yo is set
((o,r,f,x) | (Sphere (f,r))) . yo is set
(id (Tcircle (f,r))) . yo is set
(o,r,f,x) . yo is set
f1 is Element of the carrier of (o,f,r)
dom (id (Tcircle (f,r))) is non empty Element of bool the carrier of (Tcircle (f,r))
bool the carrier of (Tcircle (f,r)) is non empty set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
o is V11() ext-real real Element of REAL
the carrier of r --> o is non empty V16() V19( the carrier of r) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of r,REAL:]
[: the carrier of r,REAL:] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of r,REAL:] is non empty set
c₆ is V140() V141() V142() Element of bool REAL
( the carrier of r --> o) " c₆ is Element of bool the carrier of r
bool the carrier of r is non empty set
dom ( the carrier of r --> o) is non empty Element of bool the carrier of r
rng ( the carrier of r --> o) is non empty V140() V141() V142() Element of bool REAL
{o} is non empty trivial V140() V141() V142() set
(rng ( the carrier of r --> o)) /\ c₆ is V140() V141() V142() Element of bool REAL
( the carrier of r --> o) " ((rng ( the carrier of r --> o)) /\ c₆) is Element of bool the carrier of r
( the carrier of r --> o) " (rng ( the carrier of r --> o)) is Element of bool the carrier of r
[#] r is non empty non proper open closed Element of bool the carrier of r
(rng ( the carrier of r --> o)) /\ c₆ is V140() V141() V142() Element of bool REAL
( the carrier of r --> o) " ((rng ( the carrier of r --> o)) /\ c₆) is Element of bool the carrier of r
( the carrier of r --> o) " {} is empty trivial proper 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() open closed Element of bool the carrier of r
{} r is empty trivial proper 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() open closed Element of bool the carrier of r
o is non empty V11() ext-real positive non negative real set
f is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(2,f,o) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL 2
cl_Ball (f,o) is non empty closed V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (cl_Ball (f,o)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of (2,f,o) is non empty set
[: the carrier of (2,f,o), the carrier of (2,f,o):] is non empty V16() set
bool [: the carrier of (2,f,o), the carrier of (2,f,o):] is non empty set
Tcircle (f,o) is non empty strict TopSpace-like pathwise_connected V236() SubSpace of TOP-REAL 2
f `1 is V11() ext-real real Element of REAL
f `2 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
[:(TOP-REAL 2),(TOP-REAL 2):] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] is non empty set
x is V11() ext-real real Element of REAL
the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> x is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
[: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:] is non empty set
g is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
W is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
yo is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[W,yo] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{W,yo} is non empty functional set
{W} is non empty trivial functional set
{{W,yo},{W}} is non empty set
yo `1 is V11() ext-real real Element of REAL
(yo `1) - (f `1) is V11() ext-real real Element of REAL
g is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
W is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
yo is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
f1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[yo,f1] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{yo,f1} is non empty functional set
{yo} is non empty trivial functional set
{{yo,f1},{yo}} is non empty set
f1 `1 is V11() ext-real real Element of REAL
W is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
yo is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
f1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
D2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[f1,D2] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{f1,D2} is non empty functional set
{f1} is non empty trivial functional set
{{f1,D2},{f1}} is non empty set
D2 `2 is V11() ext-real real Element of REAL
(D2 `2) - (f `2) is V11() ext-real real Element of REAL
yo is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
((TOP-REAL 2),(TOP-REAL 2)) is Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of the carrier of (TOP-REAL 2) : not b₁ = b₂ } is set
[:(2,f,o),(2,f,o):] is non empty strict TopSpace-like TopStruct
the carrier of [:(2,f,o),(2,f,o):] is non empty set
((TOP-REAL 2),(TOP-REAL 2)) /\ the carrier of [:(2,f,o),(2,f,o):] is Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
the carrier of (Tcircle (f,o)) is non empty set
the Element of the carrier of (Tcircle (f,o)) is Element of the carrier of (Tcircle (f,o))
f - f is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- f is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
- f is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
K269((TOP-REAL 2),f,(- f)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
f + (- f) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
f - f is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.(f - f).| is V11() ext-real non negative real Element of REAL
0. (TOP-REAL 2) is V16() Function-like V50(2) V51() V68( TOP-REAL 2) complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
|.(0. (TOP-REAL 2)).| is V11() ext-real non negative real Element of REAL
Sphere (f,o) is non empty closed V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Ball (f,o) is non empty open V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
[f, the Element of the carrier of (Tcircle (f,o))] is non empty Element of the carrier of [:(TOP-REAL 2),(Tcircle (f,o)):]
[:(TOP-REAL 2),(Tcircle (f,o)):] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL 2),(Tcircle (f,o)):] is non empty set
{f, the Element of the carrier of (Tcircle (f,o))} is non empty set
{f} is non empty trivial functional set
{{f, the Element of the carrier of (Tcircle (f,o))},{f}} is non empty set
f1 is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
OK is non empty Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
f1 | OK is non empty V16() V19(OK) V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
[:(TOP-REAL 2),(TOP-REAL 2):] | OK is non empty strict TopSpace-like SubSpace of [:(TOP-REAL 2),(TOP-REAL 2):]
the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) is non empty set
[: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:] is non empty set
f is non empty V16() V19( the carrier of (2,f,o)) V20( the carrier of (2,f,o)) Function-like total quasi_total continuous Element of bool [: the carrier of (2,f,o), the carrier of (2,f,o):]
(2,o,f,f) is non empty V16() V19( the carrier of (2,f,o)) V20( the carrier of (Tcircle (f,o))) Function-like total quasi_total Element of bool [: the carrier of (2,f,o), the carrier of (Tcircle (f,o)):]
[: the carrier of (2,f,o), the carrier of (Tcircle (f,o)):] is non empty V16() set
bool [: the carrier of (2,f,o), the carrier of (Tcircle (f,o)):] is non empty set
dy is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
fy2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
dx is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[fy2,dx] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{fy2,dx} is non empty functional set
{fy2} is non empty trivial functional set
{{fy2,dx},{fy2}} is non empty set
fy2 `2 is V11() ext-real real Element of REAL
dx `2 is V11() ext-real real Element of REAL
(fy2 `2) - (dx `2) is V11() ext-real real Element of REAL
dy is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
fy2 is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
dx is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
Dx is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[dx,Dx] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{dx,Dx} is non empty functional set
{dx} is non empty trivial functional set
{{dx,Dx},{dx}} is non empty set
Dx `2 is V11() ext-real real Element of REAL
fy2 is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
dx is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Dx is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
Dy is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[Dx,Dy] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{Dx,Dy} is non empty functional set
{Dx} is non empty trivial functional set
{{Dx,Dy},{Dx}} is non empty set
Dx `1 is V11() ext-real real Element of REAL
Dy `1 is V11() ext-real real Element of REAL
(Dx `1) - (Dy `1) is V11() ext-real real Element of REAL
dx is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
[: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:] is non empty set
Yo is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:]
yo is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Yo . yo is V11() ext-real real Element of the carrier of R^1
xo is V140() V141() V142() Element of bool the carrier of R^1
Zxo is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
p2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[Zxo,p2] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{Zxo,p2} is non empty functional set
{Zxo} is non empty trivial functional set
{{Zxo,p2},{Zxo}} is non empty set
p2 `2 is V11() ext-real real Element of REAL
(p2 `2) - (f `2) is V11() ext-real real Element of REAL
Zyo is V140() V141() V142() open Element of bool REAL
dy is V11() ext-real real set
((p2 `2) - (f `2)) - dy is V11() ext-real real Element of REAL
((p2 `2) - (f `2)) + dy is V11() ext-real real Element of REAL
].(((p2 `2) - (f `2)) - dy),(((p2 `2) - (f `2)) + dy).[ is V140() V141() V142() open Element of bool REAL
dx is V11() ext-real real Element of REAL
(p2 `2) - dx is V11() ext-real real Element of REAL
(p2 `2) + dx is V11() ext-real real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() ext-real real Element of REAL : ( not b₂ <= (p2 `2) - dx & not (p2 `2) + dx <= b₂ ) } is set
Zdx is set
m is V11() ext-real real Element of REAL
fy2 is V11() ext-real real Element of REAL
|[m,fy2]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[#] (TOP-REAL 2) is non empty non proper open closed Element of bool the carrier of (TOP-REAL 2)
Zdx is Element of bool the carrier of (TOP-REAL 2)
[:([#] (TOP-REAL 2)),Zdx:] is V16() Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Yo .: [:([#] (TOP-REAL 2)),Zdx:] is V140() V141() V142() Element of bool the carrier of R^1
p2 `1 is V11() ext-real real Element of REAL
|[(p2 `1),(p2 `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(p2 `2) - 0 is V11() ext-real real Element of REAL
(p2 `2) + 0 is V11() ext-real real Element of REAL
m is set
fy2 is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Yo . fy2 is V11() ext-real real Element of the carrier of R^1
yo . fy2 is V11() ext-real real Element of REAL
fx2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
yy is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[fx2,yy] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{fx2,yy} is non empty functional set
{fx2} is non empty trivial functional set
{{fx2,yy},{fx2}} is non empty set
yy `2 is V11() ext-real real Element of REAL
(yy `2) - (f `2) is V11() ext-real real Element of REAL
xx is V11() ext-real real Element of REAL
Zfy2 is V11() ext-real real Element of REAL
|[xx,Zfy2]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
((p2 `2) - dx) - (f `2) is V11() ext-real real Element of REAL
((p2 `2) + dx) - (f `2) is V11() ext-real real Element of REAL
((p2 `2) - (f `2)) - dx is V11() ext-real real Element of REAL
((p2 `2) - (f `2)) + dx is V11() ext-real real Element of REAL
].(((p2 `2) - (f `2)) - dx),(((p2 `2) - (f `2)) + dx).[ is V140() V141() V142() open Element of bool REAL
Xo is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:]
xo is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Xo . xo is V11() ext-real real Element of the carrier of R^1
Zyo is V140() V141() V142() Element of bool the carrier of R^1
p2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
g is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[p2,g] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{p2,g} is non empty functional set
{p2} is non empty trivial functional set
{{p2,g},{p2}} is non empty set
g `1 is V11() ext-real real Element of REAL
(g `1) - (f `1) is V11() ext-real real Element of REAL
Zxo is V140() V141() V142() open Element of bool REAL
dx is V11() ext-real real set
((g `1) - (f `1)) - dx is V11() ext-real real Element of REAL
((g `1) - (f `1)) + dx is V11() ext-real real Element of REAL
].(((g `1) - (f `1)) - dx),(((g `1) - (f `1)) + dx).[ is V140() V141() V142() open Element of bool REAL
Zdy is V11() ext-real real Element of REAL
(g `1) - Zdy is V11() ext-real real Element of REAL
(g `1) + Zdy is V11() ext-real real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() ext-real real Element of REAL : ( not b<sub>1</sub> <= (g `1) - Zdy & not (g `1) + Zdy <= b<sub>1</sub> ) } is set
m is set
fy2 is V11() ext-real real Element of REAL
fx2 is V11() ext-real real Element of REAL
|[fy2,fx2]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[#] (TOP-REAL 2) is non empty non proper open closed Element of bool the carrier of (TOP-REAL 2)
m is Element of bool the carrier of (TOP-REAL 2)
[:([#] (TOP-REAL 2)),m:] is V16() Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Xo .: [:([#] (TOP-REAL 2)),m:] is V140() V141() V142() Element of bool the carrier of R^1
g `2 is V11() ext-real real Element of REAL
|[(g `1),(g `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(g `1) - 0 is V11() ext-real real Element of REAL
(g `1) + 0 is V11() ext-real real Element of REAL
fy2 is set
fx2 is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Xo . fx2 is V11() ext-real real Element of the carrier of R^1
g . fx2 is V11() ext-real real Element of REAL
yy is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
xx is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[yy,xx] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{yy,xx} is non empty functional set
{yy} is non empty trivial functional set
{{yy,xx},{yy}} is non empty set
xx `1 is V11() ext-real real Element of REAL
(xx `1) - (f `1) is V11() ext-real real Element of REAL
Zfy2 is V11() ext-real real Element of REAL
Zfx2 is V11() ext-real real Element of REAL
|[Zfy2,Zfx2]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
((g `1) - Zdy) - (f `1) is V11() ext-real real Element of REAL
((g `1) + Zdy) - (f `1) is V11() ext-real real Element of REAL
((g `1) - (f `1)) - Zdy is V11() ext-real real Element of REAL
((g `1) - (f `1)) + Zdy is V11() ext-real real Element of REAL
].(((g `1) - (f `1)) - Zdy),(((g `1) - (f `1)) + Zdy).[ is V140() V141() V142() open Element of bool REAL
yo is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
yo | OK is non empty V16() V19(OK) V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
xo is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
xo | OK is non empty V16() V19(OK) V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(xo | OK) (#) (xo | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(yo | OK) (#) (yo | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK)) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
Dy is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:]
dy is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Dy . dy is V11() ext-real real Element of the carrier of R^1
dx is V140() V141() V142() Element of bool the carrier of R^1
dy . dy is V11() ext-real real Element of REAL
Zdx is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
m is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[Zdx,m] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{Zdx,m} is non empty functional set
{Zdx} is non empty trivial functional set
{{Zdx,m},{Zdx}} is non empty set
Zdx `2 is V11() ext-real real Element of REAL
m `2 is V11() ext-real real Element of REAL
(Zdx `2) - (m `2) is V11() ext-real real Element of REAL
Zdy is V140() V141() V142() open Element of bool REAL
fx2 is V11() ext-real real set
((Zdx `2) - (m `2)) - fx2 is V11() ext-real real Element of REAL
((Zdx `2) - (m `2)) + fx2 is V11() ext-real real Element of REAL
].(((Zdx `2) - (m `2)) - fx2),(((Zdx `2) - (m `2)) + fx2).[ is V140() V141() V142() open Element of bool REAL
yy is V11() ext-real real Element of REAL
yy / 2 is V11() ext-real real Element of REAL
(m `2) - (yy / 2) is V11() ext-real real Element of REAL
(m `2) + (yy / 2) is V11() ext-real real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() ext-real real Element of REAL : ( not b<sub>2</sub> <= (m `2) - (yy / 2) & not (m `2) + (yy / 2) <= b<sub>2</sub> ) } is set
Zfy2 is set
Zfx2 is V11() ext-real real Element of REAL
p1 is V11() ext-real real Element of REAL
|[Zfx2,p1]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
m `1 is V11() ext-real real Element of REAL
|[(m `1),(m `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
0 / 2 is empty trivial V11() ext-real non positive non negative real 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() Element of REAL
(m `2) - 0 is V11() ext-real real Element of REAL
(m `2) + 0 is V11() ext-real real Element of REAL
Zfy2 is Element of bool the carrier of (TOP-REAL 2)
(Zdx `2) - (yy / 2) is V11() ext-real real Element of REAL
(Zdx `2) + (yy / 2) is V11() ext-real real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() ext-real real Element of REAL : ( not b₂ <= (Zdx `2) - (yy / 2) & not (Zdx `2) + (yy / 2) <= b₂ ) } is set
p1 is set
m is V11() ext-real real Element of REAL
p2 is V11() ext-real real Element of REAL
|[m,p2]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
[:p1,Zfy2:] is V16() Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Dy .: [:p1,Zfy2:] is V140() V141() V142() Element of bool the carrier of R^1
Zdx `1 is V11() ext-real real Element of REAL
|[(Zdx `1),(Zdx `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(Zdx `2) - 0 is V11() ext-real real Element of REAL
(Zdx `2) + 0 is V11() ext-real real Element of REAL
m is set
p2 is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Dy . p2 is V11() ext-real real Element of the carrier of R^1
dy . p2 is V11() ext-real real Element of REAL
pp is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
k is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[pp,k] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{pp,k} is non empty functional set
{pp} is non empty trivial functional set
{{pp,k},{pp}} is non empty set
pp `2 is V11() ext-real real Element of REAL
k `2 is V11() ext-real real Element of REAL
(pp `2) - (k `2) is V11() ext-real real Element of REAL
x3 is V11() ext-real real Element of REAL
y3 is V11() ext-real real Element of REAL
|[x3,y3]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(m `2) - y3 is V11() ext-real real Element of REAL
(m `2) - ((m `2) + (yy / 2)) is V11() ext-real real Element of REAL
- (yy / 2) is V11() ext-real real Element of REAL
y3 + (yy / 2) is V11() ext-real real Element of REAL
((m `2) - (yy / 2)) + (yy / 2) is V11() ext-real real Element of REAL
(y3 + (yy / 2)) - y3 is V11() ext-real real Element of REAL
abs ((m `2) - y3) is V11() ext-real real Element of REAL
X3 is V11() ext-real real Element of REAL
Y3 is V11() ext-real real Element of REAL
|[X3,Y3]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(Zdx `2) - Y3 is V11() ext-real real Element of REAL
(Zdx `2) - ((Zdx `2) + (yy / 2)) is V11() ext-real real Element of REAL
((Zdx `2) - Y3) - ((m `2) - y3) is V11() ext-real real Element of REAL
abs (((Zdx `2) - Y3) - ((m `2) - y3)) is V11() ext-real real Element of REAL
abs ((Zdx `2) - Y3) is V11() ext-real real Element of REAL
(abs ((Zdx `2) - Y3)) + (abs ((m `2) - y3)) is V11() ext-real real Element of REAL
- (((Zdx `2) - Y3) - ((m `2) - y3)) is V11() ext-real real Element of REAL
abs (- (((Zdx `2) - Y3) - ((m `2) - y3))) is V11() ext-real real Element of REAL
Y3 + (yy / 2) is V11() ext-real real Element of REAL
((Zdx `2) - (yy / 2)) + (yy / 2) is V11() ext-real real Element of REAL
(Y3 + (yy / 2)) - Y3 is V11() ext-real real Element of REAL
(yy / 2) + (yy / 2) is V11() ext-real real Element of REAL
Y3 - y3 is V11() ext-real real Element of REAL
(Y3 - y3) - ((Zdx `2) - (m `2)) is V11() ext-real real Element of REAL
abs ((Y3 - y3) - ((Zdx `2) - (m `2))) is V11() ext-real real Element of REAL
((Zdx `2) - (m `2)) - yy is V11() ext-real real Element of REAL
((Zdx `2) - (m `2)) + yy is V11() ext-real real Element of REAL
].(((Zdx `2) - (m `2)) - yy),(((Zdx `2) - (m `2)) + yy).[ is V140() V141() V142() open Element of bool REAL
Dx is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:]
dx is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Dx . dx is V11() ext-real real Element of the carrier of R^1
Zdy is V140() V141() V142() Element of bool the carrier of R^1
dx . dx is V11() ext-real real Element of REAL
m is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
fy2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[m,fy2] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{m,fy2} is non empty functional set
{m} is non empty trivial functional set
{{m,fy2},{m}} is non empty set
m `1 is V11() ext-real real Element of REAL
fy2 `1 is V11() ext-real real Element of REAL
(m `1) - (fy2 `1) is V11() ext-real real Element of REAL
Zdx is V140() V141() V142() open Element of bool REAL
yy is V11() ext-real real set
((m `1) - (fy2 `1)) - yy is V11() ext-real real Element of REAL
((m `1) - (fy2 `1)) + yy is V11() ext-real real Element of REAL
].(((m `1) - (fy2 `1)) - yy),(((m `1) - (fy2 `1)) + yy).[ is V140() V141() V142() open Element of bool REAL
xx is V11() ext-real real Element of REAL
xx / 2 is V11() ext-real real Element of REAL
(fy2 `1) - (xx / 2) is V11() ext-real real Element of REAL
(fy2 `1) + (xx / 2) is V11() ext-real real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() ext-real real Element of REAL : ( not b<sub>1</sub> <= (fy2 `1) - (xx / 2) & not (fy2 `1) + (xx / 2) <= b<sub>1</sub> ) } is set
Zfx2 is set
p1 is V11() ext-real real Element of REAL
m is V11() ext-real real Element of REAL
|[p1,m]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
fy2 `2 is V11() ext-real real Element of REAL
|[(fy2 `1),(fy2 `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
0 / 2 is empty trivial V11() ext-real non positive non negative real 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() Element of REAL
(fy2 `1) - 0 is V11() ext-real real Element of REAL
(fy2 `1) + 0 is V11() ext-real real Element of REAL
Zfx2 is Element of bool the carrier of (TOP-REAL 2)
(m `1) - (xx / 2) is V11() ext-real real Element of REAL
(m `1) + (xx / 2) is V11() ext-real real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() ext-real real Element of REAL : ( not b₁ <= (m `1) - (xx / 2) & not (m `1) + (xx / 2) <= b₁ ) } is set
m is set
p2 is V11() ext-real real Element of REAL
pp is V11() ext-real real Element of REAL
|[p2,pp]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
m is Element of bool the carrier of (TOP-REAL 2)
[:m,Zfx2:] is V16() Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Dx .: [:m,Zfx2:] is V140() V141() V142() Element of bool the carrier of R^1
m `2 is V11() ext-real real Element of REAL
|[(m `1),(m `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(m `1) - 0 is V11() ext-real real Element of REAL
(m `1) + 0 is V11() ext-real real Element of REAL
p2 is set
pp is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
Dx . pp is V11() ext-real real Element of the carrier of R^1
dx . pp is V11() ext-real real Element of REAL
k is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
x3 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[k,x3] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{k,x3} is non empty functional set
{k} is non empty trivial functional set
{{k,x3},{k}} is non empty set
k `1 is V11() ext-real real Element of REAL
x3 `1 is V11() ext-real real Element of REAL
(k `1) - (x3 `1) is V11() ext-real real Element of REAL
y3 is V11() ext-real real Element of REAL
X3 is V11() ext-real real Element of REAL
|[y3,X3]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(fy2 `1) - y3 is V11() ext-real real Element of REAL
(fy2 `1) - ((fy2 `1) + (xx / 2)) is V11() ext-real real Element of REAL
- (xx / 2) is V11() ext-real real Element of REAL
y3 + (xx / 2) is V11() ext-real real Element of REAL
((fy2 `1) - (xx / 2)) + (xx / 2) is V11() ext-real real Element of REAL
(y3 + (xx / 2)) - y3 is V11() ext-real real Element of REAL
abs ((fy2 `1) - y3) is V11() ext-real real Element of REAL
Y3 is V11() ext-real real Element of REAL
F is V11() ext-real real Element of REAL
|[Y3,F]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(m `1) - Y3 is V11() ext-real real Element of REAL
(m `1) - ((m `1) + (xx / 2)) is V11() ext-real real Element of REAL
((m `1) - Y3) - ((fy2 `1) - y3) is V11() ext-real real Element of REAL
abs (((m `1) - Y3) - ((fy2 `1) - y3)) is V11() ext-real real Element of REAL
abs ((m `1) - Y3) is V11() ext-real real Element of REAL
(abs ((m `1) - Y3)) + (abs ((fy2 `1) - y3)) is V11() ext-real real Element of REAL
- (((m `1) - Y3) - ((fy2 `1) - y3)) is V11() ext-real real Element of REAL
abs (- (((m `1) - Y3) - ((fy2 `1) - y3))) is V11() ext-real real Element of REAL
Y3 + (xx / 2) is V11() ext-real real Element of REAL
((m `1) - (xx / 2)) + (xx / 2) is V11() ext-real real Element of REAL
(Y3 + (xx / 2)) - Y3 is V11() ext-real real Element of REAL
(xx / 2) + (xx / 2) is V11() ext-real real Element of REAL
Y3 - y3 is V11() ext-real real Element of REAL
(Y3 - y3) - ((m `1) - (fy2 `1)) is V11() ext-real real Element of REAL
abs ((Y3 - y3) - ((m `1) - (fy2 `1))) is V11() ext-real real Element of REAL
((m `1) - (fy2 `1)) - xx is V11() ext-real real Element of REAL
((m `1) - (fy2 `1)) + xx is V11() ext-real real Element of REAL
].(((m `1) - (fy2 `1)) - xx),(((m `1) - (fy2 `1)) + xx).[ is V140() V141() V142() open Element of bool REAL
dy is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
dy | OK is non empty V16() V19(OK) V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
dx is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
dx | OK is non empty V16() V19(OK) V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(dx | OK) (#) (dx | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(dy | OK) (#) (dy | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK)) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
fY2 is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:]
fy2 is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
fY2 . fy2 is V11() ext-real real Element of the carrier of R^1
fx2 is V140() V141() V142() Element of bool the carrier of R^1
xx is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
Zfy2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[xx,Zfy2] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{xx,Zfy2} is non empty functional set
{xx} is non empty trivial functional set
{{xx,Zfy2},{xx}} is non empty set
Zfy2 `2 is V11() ext-real real Element of REAL
yy is V140() V141() V142() open Element of bool REAL
Zfx2 is V11() ext-real real set
(Zfy2 `2) - Zfx2 is V11() ext-real real Element of REAL
(Zfy2 `2) + Zfx2 is V11() ext-real real Element of REAL
].((Zfy2 `2) - Zfx2),((Zfy2 `2) + Zfx2).[ is V140() V141() V142() open Element of bool REAL
p1 is V11() ext-real real Element of REAL
(Zfy2 `2) - p1 is V11() ext-real real Element of REAL
(Zfy2 `2) + p1 is V11() ext-real real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() ext-real real Element of REAL : ( not b₂ <= (Zfy2 `2) - p1 & not (Zfy2 `2) + p1 <= b₂ ) } is set
p2 is set
pp is V11() ext-real real Element of REAL
k is V11() ext-real real Element of REAL
|[pp,k]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[#] (TOP-REAL 2) is non empty non proper open closed Element of bool the carrier of (TOP-REAL 2)
p2 is Element of bool the carrier of (TOP-REAL 2)
[:([#] (TOP-REAL 2)),p2:] is V16() Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
fY2 .: [:([#] (TOP-REAL 2)),p2:] is V140() V141() V142() Element of bool the carrier of R^1
Zfy2 `1 is V11() ext-real real Element of REAL
|[(Zfy2 `1),(Zfy2 `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(Zfy2 `2) - 0 is V11() ext-real real Element of REAL
(Zfy2 `2) + 0 is V11() ext-real real Element of REAL
pp is set
k is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
fY2 . k is V11() ext-real real Element of the carrier of R^1
x3 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
y3 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[x3,y3] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{x3,y3} is non empty functional set
{x3} is non empty trivial functional set
{{x3,y3},{x3}} is non empty set
y3 `2 is V11() ext-real real Element of REAL
X3 is V11() ext-real real Element of REAL
Y3 is V11() ext-real real Element of REAL
|[X3,Y3]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(Zfy2 `2) - Y3 is V11() ext-real real Element of REAL
(Zfy2 `2) - ((Zfy2 `2) + p1) is V11() ext-real real Element of REAL
- p1 is V11() ext-real real Element of REAL
Y3 + p1 is V11() ext-real real Element of REAL
((Zfy2 `2) - p1) + p1 is V11() ext-real real Element of REAL
(Y3 + p1) - Y3 is V11() ext-real real Element of REAL
abs ((Zfy2 `2) - Y3) is V11() ext-real real Element of REAL
- ((Zfy2 `2) - Y3) is V11() ext-real real Element of REAL
abs (- ((Zfy2 `2) - Y3)) is V11() ext-real real Element of REAL
Y3 - (Zfy2 `2) is V11() ext-real real Element of REAL
abs (Y3 - (Zfy2 `2)) is V11() ext-real real Element of REAL
].((Zfy2 `2) - p1),((Zfy2 `2) + p1).[ is V140() V141() V142() open Element of bool REAL
fX2 is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):], the carrier of R^1:]
fx2 is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
fX2 . fx2 is V11() ext-real real Element of the carrier of R^1
yy is V140() V141() V142() Element of bool the carrier of R^1
Zfy2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
Zfx2 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[Zfy2,Zfx2] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{Zfy2,Zfx2} is non empty functional set
{Zfy2} is non empty trivial functional set
{{Zfy2,Zfx2},{Zfy2}} is non empty set
Zfx2 `1 is V11() ext-real real Element of REAL
xx is V140() V141() V142() open Element of bool REAL
p1 is V11() ext-real real set
(Zfx2 `1) - p1 is V11() ext-real real Element of REAL
(Zfx2 `1) + p1 is V11() ext-real real Element of REAL
].((Zfx2 `1) - p1),((Zfx2 `1) + p1).[ is V140() V141() V142() open Element of bool REAL
m is V11() ext-real real Element of REAL
(Zfx2 `1) - m is V11() ext-real real Element of REAL
(Zfx2 `1) + m is V11() ext-real real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() ext-real real Element of REAL : ( not b<sub>1</sub> <= (Zfx2 `1) - m & not (Zfx2 `1) + m <= b<sub>1</sub> ) } is set
pp is set
k is V11() ext-real real Element of REAL
x3 is V11() ext-real real Element of REAL
|[k,x3]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[#] (TOP-REAL 2) is non empty non proper open closed Element of bool the carrier of (TOP-REAL 2)
pp is Element of bool the carrier of (TOP-REAL 2)
[:([#] (TOP-REAL 2)),pp:] is V16() Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
fX2 .: [:([#] (TOP-REAL 2)),pp:] is V140() V141() V142() Element of bool the carrier of R^1
Zfx2 `2 is V11() ext-real real Element of REAL
|[(Zfx2 `1),(Zfx2 `2)]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(Zfx2 `1) - 0 is V11() ext-real real Element of REAL
(Zfx2 `1) + 0 is V11() ext-real real Element of REAL
k is set
x3 is Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
fX2 . x3 is V11() ext-real real Element of the carrier of R^1
y3 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
X3 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[y3,X3] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{y3,X3} is non empty functional set
{y3} is non empty trivial functional set
{{y3,X3},{y3}} is non empty set
X3 `1 is V11() ext-real real Element of REAL
Y3 is V11() ext-real real Element of REAL
F is V11() ext-real real Element of REAL
|[Y3,F]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(Zfx2 `1) - Y3 is V11() ext-real real Element of REAL
(Zfx2 `1) - ((Zfx2 `1) + m) is V11() ext-real real Element of REAL
- m is V11() ext-real real Element of REAL
Y3 + m is V11() ext-real real Element of REAL
((Zfx2 `1) - m) + m is V11() ext-real real Element of REAL
(Y3 + m) - Y3 is V11() ext-real real Element of REAL
abs ((Zfx2 `1) - Y3) is V11() ext-real real Element of REAL
- ((Zfx2 `1) - Y3) is V11() ext-real real Element of REAL
abs (- ((Zfx2 `1) - Y3)) is V11() ext-real real Element of REAL
Y3 - (Zfx2 `1) is V11() ext-real real Element of REAL
abs (Y3 - (Zfx2 `1)) is V11() ext-real real Element of REAL
].((Zfx2 `1) - m),((Zfx2 `1) + m).[ is V140() V141() V142() open Element of bool REAL
(yo | OK) (#) (dy | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(xo | OK) (#) (dx | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
fy2 is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
fy2 | OK is non empty V16() V19(OK) V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
fx2 is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):],REAL:]
fx2 | OK is non empty V16() V19(OK) V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) is non empty Element of bool OK
bool OK is non empty set
m is Element of the carrier of (2,f,o)
p2 is Element of the carrier of (2,f,o)
[m,p2] is non empty Element of the carrier of [:(2,f,o),(2,f,o):]
{m,p2} is non empty set
{m} is non empty trivial set
{{m,p2},{m}} is non empty set
m is V11() ext-real real set
rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) is non empty V140() V141() V142() Element of bool REAL
p2 is set
((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . p2 is V11() ext-real real set
pp is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
k is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[pp,k] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{pp,k} is non empty functional set
{pp} is non empty trivial functional set
{{pp,k},{pp}} is non empty set
x3 is Element of the carrier of (2,f,o)
y3 is Element of the carrier of (2,f,o)
[x3,y3] is non empty Element of the carrier of [:(2,f,o),(2,f,o):]
{x3,y3} is non empty set
{x3} is non empty trivial set
{{x3,y3},{x3}} is non empty set
(f1 | OK) . [pp,k] is V11() ext-real real set
f1 . [pp,k] is V11() ext-real real Element of REAL
k `1 is V11() ext-real real Element of REAL
(k `1) - (f `1) is V11() ext-real real Element of REAL
k `2 is V11() ext-real real Element of REAL
(k `2) - (f `2) is V11() ext-real real Element of REAL
xo . [pp,k] is V11() ext-real real Element of REAL
F is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
F is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[F,F] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{F,F} is non empty functional set
{F} is non empty trivial functional set
{{F,F},{F}} is non empty set
F `1 is V11() ext-real real Element of REAL
(F `1) - (f `1) is V11() ext-real real Element of REAL
k - f is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
K269((TOP-REAL 2),k,(- f)) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
k + (- f) is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
k - f is V16() V19( NAT ) V20( REAL ) Function-like V51() complex-yielding V131() V132() M7( REAL )
|.(k - f).| is V11() ext-real non negative real Element of REAL
|.(k - f).| ^2 is V11() ext-real real Element of REAL
|.(k - f).| * |.(k - f).| is V11() ext-real non negative real set
yo . [pp,k] is V11() ext-real real Element of REAL
p is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
V is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[p,V] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{p,V} is non empty functional set
{p} is non empty trivial functional set
{{p,V},{p}} is non empty set
V `2 is V11() ext-real real Element of REAL
(V `2) - (f `2) is V11() ext-real real Element of REAL
(xo | OK) . [pp,k] is V11() ext-real real set
(yo | OK) . [pp,k] is V11() ext-real real set
(k - f) `1 is V11() ext-real real Element of REAL
((k - f) `1) ^2 is V11() ext-real real Element of REAL
((k - f) `1) * ((k - f) `1) is V11() ext-real non negative real set
(k - f) `2 is V11() ext-real real Element of REAL
((k - f) `2) ^2 is V11() ext-real real Element of REAL
((k - f) `2) * ((k - f) `2) is V11() ext-real non negative real set
(((k - f) `1) ^2) + (((k - f) `2) ^2) is V11() ext-real real Element of REAL
((k `1) - (f `1)) ^2 is V11() ext-real real Element of REAL
((k `1) - (f `1)) * ((k `1) - (f `1)) is V11() ext-real non negative real set
(((k `1) - (f `1)) ^2) + (((k - f) `2) ^2) is V11() ext-real real Element of REAL
((k `2) - (f `2)) ^2 is V11() ext-real real Element of REAL
((k `2) - (f `2)) * ((k `2) - (f `2)) is V11() ext-real non negative real set
(((k `1) - (f `1)) ^2) + (((k `2) - (f `2)) ^2) is V11() ext-real real Element of REAL
((((k `1) - (f `1)) ^2) + (((k `2) - (f `2)) ^2)) - (o ^2) is V11() ext-real real Element of REAL
(o ^2) - (o ^2) is V11() ext-real real set
[#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) is non empty non proper open closed Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) is non empty set
((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . [pp,k] is V11() ext-real real set
(((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [pp,k] is V11() ext-real real set
((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [pp,k]) - ((f1 | OK) . [pp,k]) is V11() ext-real real set
((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [pp,k]) - (o ^2) is V11() ext-real real set
((xo | OK) (#) (xo | OK)) . [pp,k] is V11() ext-real real set
((yo | OK) (#) (yo | OK)) . [pp,k] is V11() ext-real real set
(((xo | OK) (#) (xo | OK)) . [pp,k]) + (((yo | OK) (#) (yo | OK)) . [pp,k]) is V11() ext-real real set
((((xo | OK) (#) (xo | OK)) . [pp,k]) + (((yo | OK) (#) (yo | OK)) . [pp,k])) - (o ^2) is V11() ext-real real set
((xo | OK) . [pp,k]) * ((xo | OK) . [pp,k]) is V11() ext-real non negative real set
(((xo | OK) . [pp,k]) * ((xo | OK) . [pp,k])) + (((yo | OK) (#) (yo | OK)) . [pp,k]) is V11() ext-real real set
((((xo | OK) . [pp,k]) * ((xo | OK) . [pp,k])) + (((yo | OK) (#) (yo | OK)) . [pp,k])) - (o ^2) is V11() ext-real real set
m is V11() ext-real real set
rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) is non empty V140() V141() V142() Element of bool REAL
dom (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) is non empty Element of bool OK
p2 is set
(((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . p2 is V11() ext-real real set
pp is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
k is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[pp,k] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{pp,k} is non empty functional set
{pp} is non empty trivial functional set
{{pp,k},{pp}} is non empty set
x3 is Element of the carrier of (2,f,o)
y3 is Element of the carrier of (2,f,o)
[x3,y3] is non empty Element of the carrier of [:(2,f,o),(2,f,o):]
{x3,y3} is non empty set
{x3} is non empty trivial set
{{x3,y3},{x3}} is non empty set
pp `1 is V11() ext-real real Element of REAL
k `1 is V11() ext-real real Element of REAL
(pp `1) - (k `1) is V11() ext-real real Element of REAL
pp `2 is V11() ext-real real Element of REAL
k `2 is V11() ext-real real Element of REAL
(pp `2) - (k `2) is V11() ext-real real Element of REAL
((pp `1) - (k `1)) ^2 is V11() ext-real real Element of REAL
((pp `1) - (k `1)) * ((pp `1) - (k `1)) is V11() ext-real non negative real set
((pp `2) - (k `2)) ^2 is V11() ext-real real Element of REAL
((pp `2) - (k `2)) * ((pp `2) - (k `2)) is V11() ext-real non negative real set
(((pp `1) - (k `1)) ^2) + (((pp `2) - (k `2)) ^2) is V11() ext-real real Element of REAL
dx . [pp,k] is V11() ext-real real Element of REAL
F is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
F is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[F,F] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{F,F} is non empty functional set
{F} is non empty trivial functional set
{{F,F},{F}} is non empty set
F `1 is V11() ext-real real Element of REAL
F `1 is V11() ext-real real Element of REAL
(F `1) - (F `1) is V11() ext-real real Element of REAL
(dx | OK) . [pp,k] is V11() ext-real real set
(dy | OK) . [pp,k] is V11() ext-real real set
dy . [pp,k] is V11() ext-real real Element of REAL
p is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
V is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[p,V] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{p,V} is non empty functional set
{p} is non empty trivial functional set
{{p,V},{p}} is non empty set
p `2 is V11() ext-real real Element of REAL
V `2 is V11() ext-real real Element of REAL
(p `2) - (V `2) is V11() ext-real real Element of REAL
(((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . [pp,k] is V11() ext-real real set
((dx | OK) (#) (dx | OK)) . [pp,k] is V11() ext-real real set
((dy | OK) (#) (dy | OK)) . [pp,k] is V11() ext-real real set
(((dx | OK) (#) (dx | OK)) . [pp,k]) + (((dy | OK) (#) (dy | OK)) . [pp,k]) is V11() ext-real real set
((dx | OK) . [pp,k]) * ((dx | OK) . [pp,k]) is V11() ext-real non negative real set
(((dx | OK) . [pp,k]) * ((dx | OK) . [pp,k])) + (((dy | OK) (#) (dy | OK)) . [pp,k]) is V11() ext-real real set
m is non empty V16() non-empty V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() positive-yielding nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
p2 is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total quasi_total complex-yielding V131() V132() nonpositive-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
m (#) p2 is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonpositive-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2) is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() nonnegative-yielding continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(fx2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
(fy2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) is non empty V16() V19( the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( REAL ) Function-like total total quasi_total quasi_total complex-yielding V131() V132() continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),REAL:]
[: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of R^1:] is non empty V16() complex-yielding V131() V132() set
bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of R^1:] is non empty set
X3 is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of R^1:]
Y3 is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( the carrier of R^1) Function-like total quasi_total complex-yielding V131() V132() Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of R^1:]
<:X3,Y3:> is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20([: the carrier of R^1, the carrier of R^1:]) Function-like total quasi_total Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),[: the carrier of R^1, the carrier of R^1:]:]
[: the carrier of R^1, the carrier of R^1:] is non empty V16() complex-yielding V131() V132() set
[: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),[: the carrier of R^1, the carrier of R^1:]:] is non empty V16() set
bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),[: the carrier of R^1, the carrier of R^1:]:] is non empty set
R2Homeomorphism * <:X3,Y3:> is V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( the carrier of (TOP-REAL 2)) Function-like Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of (TOP-REAL 2):]
[: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of (TOP-REAL 2):] is non empty V16() set
bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of (TOP-REAL 2):] is non empty set
dom (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) is non empty Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
F is Element of the carrier of (2,f,o)
(2,o,f,f) . F is Element of the carrier of (Tcircle (f,o))
f . F is Element of the carrier of (2,f,o)
[F,(f . F)] is non empty Element of the carrier of [:(2,f,o),(2,f,o):]
{F,(f . F)} is non empty set
{F} is non empty trivial set
{{F,(f . F)},{F}} is non empty set
(R2Homeomorphism * <:X3,Y3:>) . [F,(f . F)] is set
dom X3 is non empty Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
dom Y3 is non empty Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
(2,f,o,F,f) is Element of the carrier of (Tcircle (f,o))
p is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
V is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(2,f,V,p,o) is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[p,V] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{p,V} is non empty functional set
{p} is non empty trivial functional set
{{p,V},{p}} is non empty set
(f1 | OK) . [p,V] is V11() ext-real real set
f1 . [p,V] is V11() ext-real real Element of REAL
(xo | OK) . [p,V] is V11() ext-real real set
xo . [p,V] is V11() ext-real real Element of REAL
(yo | OK) . [p,V] is V11() ext-real real set
yo . [p,V] is V11() ext-real real Element of REAL
p `1 is V11() ext-real real Element of REAL
V `1 is V11() ext-real real Element of REAL
(p `1) - (V `1) is V11() ext-real real Element of REAL
p `2 is V11() ext-real real Element of REAL
V `2 is V11() ext-real real Element of REAL
(p `2) - (V `2) is V11() ext-real real Element of REAL
(V `1) - (f `1) is V11() ext-real real Element of REAL
(V `2) - (f `2) is V11() ext-real real Element of REAL
WW is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
SF is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[WW,SF] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{WW,SF} is non empty functional set
{WW} is non empty trivial functional set
{{WW,SF},{WW}} is non empty set
SF `1 is V11() ext-real real Element of REAL
(SF `1) - (f `1) is V11() ext-real real Element of REAL
Z is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
ZZ is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[Z,ZZ] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{Z,ZZ} is non empty functional set
{Z} is non empty trivial functional set
{{Z,ZZ},{Z}} is non empty set
ZZ `2 is V11() ext-real real Element of REAL
(ZZ `2) - (f `2) is V11() ext-real real Element of REAL
p2 . [p,V] is V11() ext-real real set
(((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [p,V] is V11() ext-real real set
((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [p,V]) - ((f1 | OK) . [p,V]) is V11() ext-real real set
((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [p,V]) - (o ^2) is V11() ext-real real set
((xo | OK) (#) (xo | OK)) . [p,V] is V11() ext-real real set
((yo | OK) (#) (yo | OK)) . [p,V] is V11() ext-real real set
(((xo | OK) (#) (xo | OK)) . [p,V]) + (((yo | OK) (#) (yo | OK)) . [p,V]) is V11() ext-real real set
((((xo | OK) (#) (xo | OK)) . [p,V]) + (((yo | OK) (#) (yo | OK)) . [p,V])) - (o ^2) is V11() ext-real real set
((xo | OK) . [p,V]) * ((xo | OK) . [p,V]) is V11() ext-real non negative real set
(((xo | OK) . [p,V]) * ((xo | OK) . [p,V])) + (((yo | OK) (#) (yo | OK)) . [p,V]) is V11() ext-real real set
((((xo | OK) . [p,V]) * ((xo | OK) . [p,V])) + (((yo | OK) (#) (yo | OK)) . [p,V])) - (o ^2) is V11() ext-real real set
((V `1) - (f `1)) ^2 is V11() ext-real real Element of REAL
((V `1) - (f `1)) * ((V `1) - (f `1)) is V11() ext-real non negative real set
((V `2) - (f `2)) ^2 is V11() ext-real real Element of REAL
((V `2) - (f `2)) * ((V `2) - (f `2)) is V11() ext-real non negative real set
(((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2) is V11() ext-real real Element of REAL
((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2) is V11() ext-real real Element of REAL
(dx | OK) . [p,V] is V11() ext-real real set
dx . [p,V] is V11() ext-real real Element of REAL
fy2 . [p,V] is V11() ext-real real Element of REAL
X1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
Y1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[X1,Y1] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{X1,Y1} is non empty functional set
{X1} is non empty trivial functional set
{{X1,Y1},{X1}} is non empty set
Y1 `2 is V11() ext-real real Element of REAL
fx2 . [p,V] is V11() ext-real real Element of REAL
XX is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
YY is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[XX,YY] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{XX,YY} is non empty functional set
{XX} is non empty trivial functional set
{{XX,YY},{XX}} is non empty set
YY `1 is V11() ext-real real Element of REAL
M is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
W1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[M,W1] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{M,W1} is non empty functional set
{M} is non empty trivial functional set
{{M,W1},{M}} is non empty set
M `1 is V11() ext-real real Element of REAL
W1 `1 is V11() ext-real real Element of REAL
(M `1) - (W1 `1) is V11() ext-real real Element of REAL
((V `1) - (f `1)) * ((p `1) - (V `1)) is V11() ext-real real Element of REAL
((V `2) - (f `2)) * ((p `2) - (V `2)) is V11() ext-real real Element of REAL
(((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))) is V11() ext-real real Element of REAL
- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) is V11() ext-real real Element of REAL
((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2 is V11() ext-real real Element of REAL
((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) * ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) is V11() ext-real non negative real set
((p `1) - (V `1)) ^2 is V11() ext-real real Element of REAL
((p `1) - (V `1)) * ((p `1) - (V `1)) is V11() ext-real non negative real set
((p `2) - (V `2)) ^2 is V11() ext-real real Element of REAL
((p `2) - (V `2)) * ((p `2) - (V `2)) is V11() ext-real non negative real set
(((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2) is V11() ext-real real Element of REAL
((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)) is V11() ext-real real Element of REAL
(((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2))) is V11() ext-real real Element of REAL
sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))) is V11() ext-real real Element of REAL
(- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2))))) is V11() ext-real real Element of REAL
((- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))))) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) is V11() ext-real real Element of REAL
((xo | OK) (#) (dx | OK)) . [p,V] is V11() ext-real real set
((xo | OK) . [p,V]) * ((dx | OK) . [p,V]) is V11() ext-real real set
((yo | OK) (#) (dy | OK)) . [p,V] is V11() ext-real real set
(dy | OK) . [p,V] is V11() ext-real real set
((yo | OK) . [p,V]) * ((dy | OK) . [p,V]) is V11() ext-real real set
dy . [p,V] is V11() ext-real real Element of REAL
a is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
a1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[a,a1] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{a,a1} is non empty functional set
{a} is non empty trivial functional set
{{a,a1},{a}} is non empty set
a `2 is V11() ext-real real Element of REAL
a1 `2 is V11() ext-real real Element of REAL
(a `2) - (a1 `2) is V11() ext-real real Element of REAL
m . [p,V] is V11() ext-real real set
((dx | OK) (#) (dx | OK)) . [p,V] is V11() ext-real real set
((dy | OK) (#) (dy | OK)) . [p,V] is V11() ext-real real set
(((dx | OK) (#) (dx | OK)) . [p,V]) + (((dy | OK) (#) (dy | OK)) . [p,V]) is V11() ext-real real set
((dx | OK) . [p,V]) * ((dx | OK) . [p,V]) is V11() ext-real non negative real set
(((dx | OK) . [p,V]) * ((dx | OK) . [p,V])) + (((dy | OK) (#) (dy | OK)) . [p,V]) is V11() ext-real real set
(((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) . [p,V] is V11() ext-real real set
(((xo | OK) (#) (dx | OK)) . [p,V]) + (((yo | OK) (#) (dy | OK)) . [p,V]) is V11() ext-real real set
((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [p,V] is V11() ext-real real set
dom (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) is non empty Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
(sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [p,V] is V11() ext-real real set
(((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) . [p,V] is V11() ext-real real set
sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) . [p,V]) is V11() ext-real real set
(m (#) p2) . [p,V] is V11() ext-real real set
(((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [p,V]) - ((m (#) p2) . [p,V]) is V11() ext-real real set
sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [p,V]) - ((m (#) p2) . [p,V])) is V11() ext-real real set
dom (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) is non empty Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
(((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) . [p,V] is V11() ext-real real set
((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [p,V] is V11() ext-real real set
(m . [p,V]) " is V11() ext-real real set
(((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [p,V]) * ((m . [p,V]) ") is V11() ext-real real set
(((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [p,V]) / (m . [p,V]) is V11() ext-real real set
(- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [p,V] is V11() ext-real real set
((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [p,V]) + ((sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [p,V]) is V11() ext-real real set
(((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [p,V]) + ((sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [p,V])) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) is V11() ext-real real Element of REAL
Y3 . [p,V] is V11() ext-real real set
(fy2 | OK) . [p,V] is V11() ext-real real set
((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [p,V] is V11() ext-real real set
((fy2 | OK) . [p,V]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [p,V]) is V11() ext-real real set
(V `2) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [p,V]) is V11() ext-real real Element of REAL
(((- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))))) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2))) * ((p `2) - (V `2)) is V11() ext-real real Element of REAL
(V `2) + ((((- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))))) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2))) * ((p `2) - (V `2))) is V11() ext-real real Element of REAL
X3 . [p,V] is V11() ext-real real set
(fx2 | OK) . [p,V] is V11() ext-real real set
((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [p,V] is V11() ext-real real set
((fx2 | OK) . [p,V]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [p,V]) is V11() ext-real real set
(V `1) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [p,V]) is V11() ext-real real Element of REAL
(((- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))))) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2))) * ((p `1) - (V `1)) is V11() ext-real real Element of REAL
(V `1) + ((((- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))))) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2))) * ((p `1) - (V `1))) is V11() ext-real real Element of REAL
|[((V `1) + ((((- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))))) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2))) * ((p `1) - (V `1)))),((V `2) + ((((- ((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2))))) + (sqrt ((((((V `1) - (f `1)) * ((p `1) - (V `1))) + (((V `2) - (f `2)) * ((p `2) - (V `2)))) ^2) - (((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2)) * (((((V `1) - (f `1)) ^2) + (((V `2) - (f `2)) ^2)) - (o ^2)))))) / ((((p `1) - (V `1)) ^2) + (((p `2) - (V `2)) ^2))) * ((p `2) - (V `2))))]| is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[(X3 . [p,V]),(Y3 . [p,V])] is non empty set
{(X3 . [p,V]),(Y3 . [p,V])} is non empty V140() V141() V142() set
{(X3 . [p,V])} is non empty trivial V140() V141() V142() set
{{(X3 . [p,V]),(Y3 . [p,V])},{(X3 . [p,V])}} is non empty set
R2Homeomorphism . [(X3 . [p,V]),(Y3 . [p,V])] is set
<:X3,Y3:> . [p,V] is set
R2Homeomorphism . (<:X3,Y3:> . [p,V]) is set
[:R^1,R^1:] is non empty strict TopSpace-like TopStruct
the carrier of [:R^1,R^1:] is non empty set
[: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of [:R^1,R^1:]:] is non empty V16() set
bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of [:R^1,R^1:]:] is non empty set
bool the carrier of (Tcircle (f,o)) is non empty set
bool the carrier of (2,f,o) is non empty set
p is Element of the carrier of (2,f,o)
(2,o,f,f) . p is Element of the carrier of (Tcircle (f,o))
V is Element of bool the carrier of (Tcircle (f,o))
[#] (Tcircle (f,o)) is non empty non proper open closed Element of bool the carrier of (Tcircle (f,o))
V1 is Element of bool the carrier of (TOP-REAL 2)
V1 /\ ([#] (Tcircle (f,o))) is Element of bool the carrier of (Tcircle (f,o))
f . p is Element of the carrier of (2,f,o)
rng R2Homeomorphism is non empty Element of bool the carrier of (TOP-REAL 2)
[#] (TOP-REAL 2) is non empty non proper open closed Element of bool the carrier of (TOP-REAL 2)
R2Homeomorphism /" is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of [:K580(),K580():]) Function-like total quasi_total Element of bool [: the carrier of (TOP-REAL 2), the carrier of [:K580(),K580():]:]
[: the carrier of (TOP-REAL 2), the carrier of [:K580(),K580():]:] is non empty V16() set
bool [: the carrier of (TOP-REAL 2), the carrier of [:K580(),K580():]:] is non empty set
(R2Homeomorphism /") .: V1 is Element of bool the carrier of [:K580(),K580():]
bool the carrier of [:K580(),K580():] is non empty set
p1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
fp is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[p1,fp] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{p1,fp} is non empty functional set
{p1} is non empty trivial functional set
{{p1,fp},{p1}} is non empty set
[p,(f . p)] is non empty Element of the carrier of [:(2,f,o),(2,f,o):]
{p,(f . p)} is non empty set
{p} is non empty trivial set
{{p,(f . p)},{p}} is non empty set
F is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( the carrier of [:R^1,R^1:]) Function-like total quasi_total continuous Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of [:R^1,R^1:]:]
R2Homeomorphism * F is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( the carrier of (TOP-REAL 2)) Function-like total quasi_total Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of (TOP-REAL 2):]
(R2Homeomorphism * F) . [p,(f . p)] is set
(R2Homeomorphism * F) . [p1,fp] is set
(R2Homeomorphism /") . ((R2Homeomorphism * F) . [p1,fp]) is set
dom R2Homeomorphism is non empty Element of bool the carrier of [:K580(),K580():]
rng F is non empty Element of bool the carrier of [:R^1,R^1:]
bool the carrier of [:R^1,R^1:] is non empty set
dom F is non empty Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
dom (R2Homeomorphism * F) is non empty Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
(R2Homeomorphism /") * (R2Homeomorphism * F) is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( the carrier of [:K580(),K580():]) Function-like total quasi_total Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of [:K580(),K580():]:]
[: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of [:K580(),K580():]:] is non empty V16() set
bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of [:K580(),K580():]:] is non empty set
((R2Homeomorphism /") * (R2Homeomorphism * F)) . [p1,fp] is set
id (dom R2Homeomorphism) is non empty V16() V19( dom R2Homeomorphism) V20( dom R2Homeomorphism) Function-like one-to-one total quasi_total Element of bool [:(dom R2Homeomorphism),(dom R2Homeomorphism):]
[:(dom R2Homeomorphism),(dom R2Homeomorphism):] is non empty V16() set
bool [:(dom R2Homeomorphism),(dom R2Homeomorphism):] is non empty set
(id (dom R2Homeomorphism)) * F is V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( dom R2Homeomorphism) Function-like Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),(dom R2Homeomorphism):]
[: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),(dom R2Homeomorphism):] is non empty V16() set
bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),(dom R2Homeomorphism):] is non empty set
W is set
((id (dom R2Homeomorphism)) * F) . W is set
F . W is set
(id (dom R2Homeomorphism)) . (F . W) is set
dom (id (dom R2Homeomorphism)) is non empty Element of bool (dom R2Homeomorphism)
bool (dom R2Homeomorphism) is non empty set
dom ((id (dom R2Homeomorphism)) * F) is Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
(R2Homeomorphism /") * R2Homeomorphism is non empty V16() V19( the carrier of [:K580(),K580():]) V20( the carrier of [:K580(),K580():]) Function-like total quasi_total Element of bool [: the carrier of [:K580(),K580():], the carrier of [:K580(),K580():]:]
[: the carrier of [:K580(),K580():], the carrier of [:K580(),K580():]:] is non empty V16() set
bool [: the carrier of [:K580(),K580():], the carrier of [:K580(),K580():]:] is non empty set
((R2Homeomorphism /") * R2Homeomorphism) * F is non empty V16() V19( the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) V20( the carrier of [:K580(),K580():]) V20( the carrier of [:R^1,R^1:]) Function-like total quasi_total quasi_total Element of bool [: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK), the carrier of [:K580(),K580():]:]
W is Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
F .: W is Element of bool the carrier of [:R^1,R^1:]
WW is Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) is Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
bool (bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]) is non empty set
SF is Element of bool (bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):])
union SF is set
Z is set
Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) is Element of bool the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)
F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) is Element of bool the carrier of [:R^1,R^1:]
X1 is Element of bool the carrier of (TOP-REAL 2)
Y1 is Element of bool the carrier of (TOP-REAL 2)
[:X1,Y1:] is V16() Element of bool the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
[#] (2,f,o) is non empty non proper open closed Element of bool the carrier of (2,f,o)
X1 /\ ([#] (2,f,o)) is Element of bool the carrier of (2,f,o)
Y1 /\ ([#] (2,f,o)) is Element of bool the carrier of (2,f,o)
YY is open Element of bool the carrier of (2,f,o)
M is Element of bool the carrier of (2,f,o)
f .: M is Element of bool the carrier of (2,f,o)
XX is open Element of bool the carrier of (2,f,o)
XX /\ M is Element of bool the carrier of (2,f,o)
W1 is Element of bool the carrier of (2,f,o)
(2,o,f,f) .: W1 is Element of bool the carrier of (Tcircle (f,o))
b is set
a is Element of the carrier of (2,f,o)
(2,o,f,f) . a is Element of the carrier of (Tcircle (f,o))
f . a is Element of the carrier of (2,f,o)
fa is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
a1 is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
[a1,fa] is non empty Element of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]
{a1,fa} is non empty functional set
{a1} is non empty trivial functional set
{{a1,fa},{a1}} is non empty set
[a,(f . a)] is non empty Element of the carrier of [:(2,f,o),(2,f,o):]
{a,(f . a)} is non empty set
{a} is non empty trivial set
{{a,(f . a)},{a}} is non empty set
[a,fa] is non empty Element of the carrier of [:(2,f,o),(TOP-REAL 2):]
[:(2,f,o),(TOP-REAL 2):] is non empty strict TopSpace-like TopStruct
the carrier of [:(2,f,o),(TOP-REAL 2):] is non empty set
{a,fa} is non empty set
{{a,fa},{a}} is non empty set
F . [a1,fa] is set
R2Homeomorphism . (F . [a1,fa]) is set
R2Homeomorphism .: ((R2Homeomorphism /") .: V1) is Element of bool the carrier of (TOP-REAL 2)
(R2Homeomorphism * F) . [a1,fa] is set
R2Homeomorphism " is V16() Function-like set
dom (R2Homeomorphism /") is non empty Element of bool the carrier of (TOP-REAL 2)
r is V11() ext-real non negative real set
o is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(2,o,r) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL 2
cl_Ball (o,r) is non empty closed V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (cl_Ball (o,r)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of (2,o,r) is non empty set
[: the carrier of (2,o,r), the carrier of (2,o,r):] is non empty V16() set
bool [: the carrier of (2,o,r), the carrier of (2,o,r):] is non empty set
f is non empty V16() V19( the carrier of (2,o,r)) V20( the carrier of (2,o,r)) Function-like total quasi_total continuous Element of bool [: the carrier of (2,o,r), the carrier of (2,o,r):]
Tcircle (o,r) is non empty strict TopSpace-like pathwise_connected SubSpace of TOP-REAL 2
the carrier of (Tcircle (o,r)) is non empty set
Sphere (o,r) is non empty closed V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
x is non empty V11() ext-real positive non negative real set
Sphere (o,x) is non empty closed V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
cl_Ball (o,x) is non empty closed V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(2,o,x) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL 2
(TOP-REAL 2) | (cl_Ball (o,x)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
Tcircle (o,x) is non empty strict TopSpace-like pathwise_connected V236() SubSpace of TOP-REAL 2
the carrier of (2,o,x) is non empty set
c₆ is non empty TopSpace-like SubSpace of (2,o,x)
the carrier of c₆ is non empty set
[: the carrier of (2,o,x), the carrier of c₆:] is non empty V16() set
bool [: the carrier of (2,o,x), the carrier of c₆:] is non empty set
(2,r,o,f) is non empty V16() V19( the carrier of (2,o,r)) V20( the carrier of (Tcircle (o,r))) Function-like total quasi_total Element of bool [: the carrier of (2,o,r), the carrier of (Tcircle (o,r)):]
[: the carrier of (2,o,r), the carrier of (Tcircle (o,r)):] is non empty V16() set
bool [: the carrier of (2,o,r), the carrier of (Tcircle (o,r)):] is non empty set
g is non empty V16() V19( the carrier of (2,o,x)) V20( the carrier of c₆) Function-like total quasi_total Element of bool [: the carrier of (2,o,x), the carrier of c₆:]
W is Element of the carrier of (2,o,x)
g . W is Element of the carrier of c₆
x is empty trivial V11() ext-real non positive non negative real 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
cl_Ball (o,x) is non empty closed V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
{o} is non empty trivial functional set
dom f is non empty Element of bool the carrier of (2,o,r)
bool the carrier of (2,o,r) is non empty set
(2,o,x) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL 2
(TOP-REAL 2) | (cl_Ball (o,x)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of (2,o,x) is non empty set
f . o is set
rng f is non empty Element of bool the carrier of (2,o,r)
r is V11() ext-real non negative real set
o is V16() Function-like V50(2) V51() complex-yielding V131() V132() Element of the carrier of (TOP-REAL 2)
(2,o,r) is non empty TopSpace-like pathwise_connected convex SubSpace of TOP-REAL 2
cl_Ball (o,r) is non empty closed V217( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (cl_Ball (o,r)) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of (2,o,r) is non empty set
[: the carrier of (2,o,r), the carrier of (2,o,r):] is non empty V16() set
bool [: the carrier of (2,o,r), the carrier of (2,o,r):] is non empty set
f is non empty V16() V19( the carrier of (2,o,r)) V20( the carrier of (2,o,r)) Function-like total quasi_total continuous Element of bool [: the carrier of (2,o,r), the carrier of (2,o,r):]
x is set
f . x is Element of the carrier of (2,o,r)
dom f is non empty Element of bool the carrier of (2,o,r)
bool the carrier of (2,o,r) is non empty set
f . x is set