:: TOPALG_6 semantic presentation

the carrier of is non empty set

{{},1} is non empty finite set

bool [:1,1:] is set

bool [:[:1,1:],1:] is set

bool [:[:1,1:],REAL:] is set

bool [:[:2,2:],REAL:] is set

bool [: the carrier of I[01], the carrier of I[01]:] is set
bool the carrier of is set

COMPLEX is non empty non trivial non finite complex-membered V171() set

TOP-REAL 2 is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() 2 -locally_euclidean V359() RLTopStruct
the carrier of () is non empty set

the carrier of is non empty set

bool the carrier of R^1 is set
bool (bool the carrier of R^1) is set

the carrier of () is non empty set
[: the carrier of R^1, the carrier of ():] is Relation-like set
bool [: the carrier of R^1, the carrier of ():] is set
CircleMap is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -defined the carrier of () -valued the carrier of () -valued Function-like total total quasi_total quasi_total onto continuous Element of bool [: the carrier of R^1, the carrier of ():]
c[10] is Element of the carrier of ()

the carrier of is non empty set

the carrier of (R^1 | (R^1 ].0,1.[)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of , the carrier of (R^1 | (R^1 ].0,1.[)):] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of , the carrier of (R^1 | (R^1 ].0,1.[)):] is set
c[-10] is Element of the carrier of ()

the carrier of is non empty set
1 / 2 is real V101() ext-real non negative Element of REAL

3 / 2 is real V101() ext-real non negative Element of REAL

R^1 ].(1 / 2),(3 / 2).[ is non empty complex-membered ext-real-membered real-membered interval Element of bool the carrier of R^1
R^1 | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like real-membered pathwise_connected interval SubSpace of R^1
the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of , the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of , the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is set

K687() is non empty V116() L10()
the carrier of K687() is non empty set
K692() is non empty V116() V223() V224() V225() V227() V253() V254() V255() V256() V257() V258() L10()
K693() is non empty V116() V225() V227() V256() V257() V258() M30(K692())
K694() is non empty V116() V223() V225() V227() V256() V257() V258() V259() M33(K692(),K693())
K696() is non empty V116() V223() V225() V227() L10()
K697() is non empty V116() V223() V225() V227() V259() M30(K696())

bool the carrier of () is set
K743(0,1) is real V101() ext-real Element of the carrier of ()
K744(0,1) is real V101() ext-real Element of the carrier of ()
bool the carrier of R^1 is set

0[01] is real V101() ext-real Element of the carrier of I[01]
1[01] is real V101() ext-real Element of the carrier of I[01]
- 1 is real V101() ext-real non positive Element of REAL

bool the carrier of I[01] is set

K745(0,1,K743(0,1),K744(0,1)) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (), the carrier of ():] is set

id the carrier of () is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one total quasi_total onto bijective V70() V72() V73() V77() complex-yielding ext-real-valued real-valued increasing non-decreasing Element of bool [: the carrier of (), the carrier of ():]
K746(0,1,K743(0,1),K744(0,1)) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]

the carrier of n is set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
[: the carrier of n, the carrier of r:] is Relation-like set
bool [: the carrier of n, the carrier of r:] is set
x is Relation-like the carrier of n -defined the carrier of r -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of r:]
bool the carrier of r is set
f is Element of bool the carrier of r
x " f is Element of bool the carrier of n
bool the carrier of n is set
rng x is Element of bool the carrier of r
bool the carrier of r is set
f is Element of the carrier of r
{f} is non empty trivial finite set
dom x is Element of bool the carrier of n
bool the carrier of n is set

g is set
x . g is set
{()} is non empty trivial finite set

[:(dom x),{()}:] is Relation-like set
bool [:(dom x),{()}:] is set
n --> f is Relation-like the carrier of n -defined the carrier of r -valued Function-like total quasi_total continuous Element of bool [: the carrier of n, the carrier of r:]
the carrier of n --> f is Relation-like the carrier of n -defined the carrier of r -valued Function-like constant total quasi_total Element of bool [: the carrier of n, the carrier of r:]
L[01] (0,1,0,1) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]
(id ()) * (id ()) is non empty Relation-like the carrier of () -defined the carrier of () -defined the carrier of () -valued the carrier of () -valued Function-like one-to-one total total quasi_total quasi_total onto bijective continuous complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]
r is real V101() ext-real set
n is real V101() ext-real set
x is real V101() ext-real set
f is real V101() ext-real set
C is real V101() ext-real set
g is real V101() ext-real set

the carrier of () is non empty complex-membered ext-real-membered real-membered set

the carrier of () is non empty complex-membered ext-real-membered real-membered set

the carrier of () is non empty complex-membered ext-real-membered real-membered set
L[01] (g,C,n,r) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (), the carrier of ():] is set
L[01] (n,r,x,f) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (), the carrier of ():] is set
(L[01] (n,r,x,f)) * (L[01] (g,C,n,r)) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (), the carrier of ():] is set
L[01] (g,C,x,f) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (), the carrier of ():]
dom ((L[01] (n,r,x,f)) * (L[01] (g,C,n,r))) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of ()
bool the carrier of () is set
[#] () is non empty non proper closed complex-membered ext-real-membered real-membered Element of bool the carrier of ()
dom (L[01] (g,C,x,f)) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of ()
U is set
((L[01] (n,r,x,f)) * (L[01] (g,C,n,r))) . U is real V101() ext-real set
(L[01] (g,C,x,f)) . U is real V101() ext-real set

V is real V101() ext-real set
rng (L[01] (g,C,n,r)) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
[#] () is non empty non proper closed complex-membered ext-real-membered real-membered Element of bool the carrier of ()
bool the carrier of () is set
(L[01] (g,C,n,r)) . U is real V101() ext-real set
dom (L[01] (g,C,n,r)) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of ()
c is real V101() ext-real set

(L[01] (n,r,x,f)) . c is real V101() ext-real set
f - x is real V101() ext-real set
r - n is real V101() ext-real set
(f - x) / (r - n) is real V101() ext-real set
c - n is real V101() ext-real set
((f - x) / (r - n)) * (c - n) is real V101() ext-real set
(((f - x) / (r - n)) * (c - n)) + x is real V101() ext-real set
((f - x) / (r - n)) * c is real V101() ext-real set
C - g is real V101() ext-real set
(r - n) / (C - g) is real V101() ext-real set
V - g is real V101() ext-real set
((r - n) / (C - g)) * (V - g) is real V101() ext-real set
(((r - n) / (C - g)) * (V - g)) + n is real V101() ext-real set
((f - x) / (r - n)) * ((((r - n) / (C - g)) * (V - g)) + n) is real V101() ext-real set
((f - x) / (r - n)) * ((r - n) / (C - g)) is real V101() ext-real set
(((f - x) / (r - n)) * ((r - n) / (C - g))) * (V - g) is real V101() ext-real set
((f - x) / (r - n)) * n is real V101() ext-real set
((((f - x) / (r - n)) * ((r - n) / (C - g))) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set
(f - x) / (C - g) is real V101() ext-real set
(r - n) / (r - n) is real V101() ext-real set
((f - x) / (C - g)) * ((r - n) / (r - n)) is real V101() ext-real set
(((f - x) / (C - g)) * ((r - n) / (r - n))) * (V - g) is real V101() ext-real set
((((f - x) / (C - g)) * ((r - n) / (r - n))) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set
((f - x) / (C - g)) * 1 is real V101() ext-real set
(((f - x) / (C - g)) * 1) * (V - g) is real V101() ext-real set
((((f - x) / (C - g)) * 1) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set
((f - x) / (C - g)) * (V - g) is real V101() ext-real set
(((f - x) / (C - g)) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set
(L[01] (n,r,x,f)) . ((L[01] (g,C,n,r)) . U) is real V101() ext-real set
n is non empty ordinal natural real V101() ext-real positive non negative set
TOP-REAL n is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() n -locally_euclidean V359() RLTopStruct
the carrier of () is non empty set

dom r is set
r .: () is set
x is set

f is set
r . f is set

g . 1 is real V101() ext-real set
Funcs ((Seg n),REAL) is non empty functional FUNCTION_DOMAIN of Seg n, REAL

dom C is set
rng C is set
{x} is non empty trivial finite set

[:(Seg n),{x}:] is Relation-like finite set
bool [:(Seg n),{x}:] is finite V29() set

rng ((Seg n) --> x) is non empty trivial finite Element of bool {x}
bool {x} is finite V29() set

r . g is set
g . 1 is real V101() ext-real set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
x is set
f is Element of the carrier of r
[#] () is non empty non proper closed Element of bool the carrier of ()
the carrier of () is non empty non trivial non finite set
bool the carrier of () is set
g is non empty a_neighborhood of f
r | g is non empty strict TopSpace-like SubSpace of r
() | ([#] ()) is non empty strict TopSpace-like SubSpace of TOP-REAL n
the carrier of (() | ([#] ())) is non empty set
the carrier of (r | g) is non empty set
[: the carrier of (() | ([#] ())), the carrier of (r | g):] is Relation-like set
bool [: the carrier of (() | ([#] ())), the carrier of (r | g):] is set
C is non empty Relation-like the carrier of (() | ([#] ())) -defined the carrier of (r | g) -valued Function-like total quasi_total Element of bool [: the carrier of (() | ([#] ())), the carrier of (r | g):]
dom C is non empty Element of bool the carrier of (() | ([#] ()))
bool the carrier of (() | ([#] ())) is set
[#] (() | ([#] ())) is non empty non proper closed Element of bool the carrier of (() | ([#] ()))
rng C is non empty Element of bool the carrier of (r | g)
bool the carrier of (r | g) is set
[#] (r | g) is non empty non proper closed Element of bool the carrier of (r | g)

TOP-REAL n is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() n -locally_euclidean V359() RLTopStruct
the carrier of () is non empty set

Sphere ((0. ()),1) is closed Element of bool the carrier of ()
bool the carrier of () is set

{r} is non empty trivial functional finite V29() set
(Sphere ((0. ()),1)) \ {r} is Element of bool the carrier of ()

TOP-REAL x is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() x -locally_euclidean V359() RLTopStruct
the carrier of () is non empty set

|.(f - (0. ())).| is real V101() ext-real non negative Element of REAL

|.(f + (- (0. ()))).| is real V101() ext-real non negative Element of REAL
- 1 is real V101() ext-real non positive set

|.(r + ((- 1) * (0. ()))).| is real V101() ext-real non negative Element of REAL

|.(r + (0. ())).| is real V101() ext-real non negative Element of REAL
|.r.| is real V101() ext-real non negative Element of REAL
|.(0. ()).| is real V101() ext-real non negative Element of REAL

g is real V101() ext-real set

|.(- r).| is real V101() ext-real non negative Element of REAL

|.((- r) + (0. ())).| is real V101() ext-real non negative Element of REAL

|.((- r) + ((- 1) * (0. ()))).| is real V101() ext-real non negative Element of REAL

|.((- r) + (- (0. ()))).| is real V101() ext-real non negative Element of REAL

|.((- f) - (0. ())).| is real V101() ext-real non negative Element of REAL
Sphere ((0. ()),1) is closed bounded Element of bool the carrier of ()
bool the carrier of () is set
n is non empty TopStruct
the carrier of n is non empty set
r is Element of the carrier of n
x is Element of the carrier of n
f is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of r,x

bool the carrier of I[01] is set
inf (dom f) is ext-real set
sup (dom f) is ext-real set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
r is Element of the carrier of n

I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]
[: the carrier of I[01], the carrier of n:] is Relation-like set
bool [: the carrier of I[01], the carrier of n:] is set
the carrier of I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
r is non empty TopSpace-like SubSpace of n
the carrier of r is non empty set
x is Element of the carrier of n
f is Element of the carrier of n
g is Element of the carrier of r
C is Element of the carrier of r
f2 is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f
x is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f
p is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C
U is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C
[: the carrier of , the carrier of r:] is Relation-like set
bool [: the carrier of , the carrier of r:] is set
V is non empty Relation-like the carrier of -defined the carrier of r -valued Function-like total quasi_total Element of bool [: the carrier of , the carrier of r:]
[: the carrier of , the carrier of n:] is Relation-like set
bool [: the carrier of , the carrier of n:] is set
c is non empty Relation-like the carrier of -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of , the carrier of n:]
p . 0 is set
p . 1 is set
f2 . 0 is set
f2 . 1 is set
fc1 is real V101() ext-real Element of the carrier of I[01]
c . (fc1,0) is set
f2 . fc1 is Element of the carrier of n
fc2 is real V101() ext-real Element of the carrier of I[01]
c . (fc2,1) is set
x . fc2 is Element of the carrier of n
c0 is real V101() ext-real Element of the carrier of I[01]
c . (0,c0) is set
f0 is real V101() ext-real Element of the carrier of I[01]
c . (1,f0) is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
r is non empty TopSpace-like SubSpace of n
the carrier of r is non empty set
x is Element of the carrier of n
f is Element of the carrier of n
Paths (x,f) is non empty set
EqRel (n,x,f) is Relation-like Paths (x,f) -defined Paths (x,f) -valued Element of bool [:(Paths (x,f)),(Paths (x,f)):]
[:(Paths (x,f)),(Paths (x,f)):] is Relation-like set
bool [:(Paths (x,f)),(Paths (x,f)):] is set
g is Element of the carrier of r
C is Element of the carrier of r
Paths (g,C) is non empty set
EqRel (r,g,C) is Relation-like Paths (g,C) -defined Paths (g,C) -valued Element of bool [:(Paths (g,C)),(Paths (g,C)):]
[:(Paths (g,C)),(Paths (g,C)):] is Relation-like set
bool [:(Paths (g,C)),(Paths (g,C)):] is set
f2 is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f
x is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f
Class ((EqRel (n,x,f)),f2) is Element of bool (Paths (x,f))
bool (Paths (x,f)) is set
Class ((EqRel (n,x,f)),x) is Element of bool (Paths (x,f))
p is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C
U is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C
Class ((EqRel (r,g,C)),p) is Element of bool (Paths (g,C))
bool (Paths (g,C)) is set
Class ((EqRel (r,g,C)),U) is Element of bool (Paths (g,C))

the carrier of n is non empty trivial finite set
r is Element of the carrier of n
FundamentalGroup (n,r) is non empty V116() V223() V224() V225() V253() V254() V255() V256() V257() V258() L10()
the carrier of (FundamentalGroup (n,r)) is non empty set
Loops r is non empty set
Paths (r,r) is non empty set
EqRel (n,r) is non empty Relation-like Loops r -defined Loops r -valued total quasi_total V70() V72() V77() Element of bool [:(),():]
[:(),():] is Relation-like set
bool [:(),():] is set
EqRel (n,r,r) is Relation-like Paths (r,r) -defined Paths (r,r) -valued Element of bool [:(Paths (r,r)),(Paths (r,r)):]
[:(Paths (r,r)),(Paths (r,r)):] is Relation-like set
bool [:(Paths (r,r)),(Paths (r,r)):] is set
f is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Path of r,r
Class ((EqRel (n,r)),f) is Element of bool ()
bool () is set
{(Class ((EqRel (n,r)),f))} is non empty trivial finite set
g is set
C is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Path of r,r
Class ((EqRel (n,r)),C) is Element of bool ()
I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]
[: the carrier of I[01], the carrier of n:] is Relation-like set
bool [: the carrier of I[01], the carrier of n:] is set
the carrier of I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]
g is set
Class (EqRel (n,r)) is a_partition of Loops r

TOP-REAL n is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() n -locally_euclidean V359() RLTopStruct
the carrier of () is non empty set
bool the carrier of () is set
[#] () is non empty non proper closed Element of bool the carrier of ()

{r} is non empty trivial functional finite V29() set
([#] ()) \ {r} is Element of bool the carrier of ()
x is Element of bool the carrier of ()

f is non empty TopSpace-like SubSpace of TOP-REAL n
[#] f is non empty non proper closed Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is set
g is Element of the carrier of f
C is Element of the carrier of f

LSeg (f2,x) is Element of bool the carrier of ()
() | (LSeg (f2,x)) is strict TopSpace-like SubSpace of TOP-REAL n
[#] (() | (LSeg (f2,x))) is non proper closed Element of bool the carrier of (() | (LSeg (f2,x)))
the carrier of (() | (LSeg (f2,x))) is set
bool the carrier of (() | (LSeg (f2,x))) is set
p is non empty TopSpace-like SubSpace of f
the carrier of p is non empty set
[: the carrier of I[01], the carrier of p:] is Relation-like set
bool [: the carrier of I[01], the carrier of p:] is set
U is non empty Relation-like the carrier of I[01] -defined the carrier of p -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of p:]
U . 0 is set
U . 1 is set
[: the carrier of I[01], the carrier of f:] is Relation-like set
bool [: the carrier of I[01], the carrier of f:] is set
V is non empty Relation-like the carrier of I[01] -defined the carrier of f -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of f:]
V . 0 is set
V . 1 is set
g is Element of the carrier of f
C is Element of the carrier of f

LSeg (f2,x) is Element of bool the carrier of ()

TOP-REAL p is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() p -locally_euclidean V359() RLTopStruct
the carrier of () is non empty set

c is real V101() ext-real Element of REAL
1 - c is real V101() ext-real set

n - 1 is real V101() ext-real set

TOP-REAL (fc2 + 1) is non empty non trivial non finite TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() fc2 + 1 -locally_euclidean V359() RLTopStruct
0. (TOP-REAL (fc2 + 1)) is Relation-like NAT -defined Function-like finite V32(fc2 + 1) V45( TOP-REAL (fc2 + 1)) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL (fc2 + 1))
the carrier of (TOP-REAL (fc2 + 1)) is non empty non trivial non finite set
the ZeroF of (TOP-REAL (fc2 + 1)) is Relation-like NAT -defined Function-like finite V32(fc2 + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL (fc2 + 1))
TPlane ((x - f2),r) is non empty TopSpace-like SubSpace of TOP-REAL n
[#] (TPlane ((x - f2),r)) is non empty non proper closed Element of bool the carrier of (TPlane ((x - f2),r))
the carrier of (TPlane ((x - f2),r)) is non empty set
bool the carrier of (TPlane ((x - f2),r)) is set
Plane ((x - f2),r) is Element of bool the carrier of ()
() | (Plane ((x - f2),r)) is strict TopSpace-like SubSpace of TOP-REAL n
[#] (() | (Plane ((x - f2),r))) is non proper closed Element of bool the carrier of (() | (Plane ((x - f2),r)))
the carrier of (() | (Plane ((x - f2),r))) is set
bool the carrier of (() | (Plane ((x - f2),r))) is set
c0 is set
c0 \ {r} is Element of bool c0
bool c0 is set
f0 is set
{ b1 where b1 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of () : |((x - f2),(b1 - r))| = 0 } is set

|((x - f2),(c1 - r))| is real V101() ext-real Element of REAL
|((x - f2),(x - f2))| is real V101() ext-real Element of REAL

LSeg (f2,c1) is Element of bool the carrier of ()

ci1 is real V101() ext-real Element of REAL
1 - ci1 is real V101() ext-real set

((1 - ci1) * U) + (ci1 * c2) is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 - ((1 - ci1) * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 + (- ((1 - ci1) * f2))) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

- (1 - ci1) is real V101() ext-real set

(c1 + ((- (1 - ci1)) * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

- 1 is real V101() ext-real non positive set
(- 1) + ci1 is real V101() ext-real set

(c1 + (((- 1) + ci1) * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

c1 + (((- 1) * f2) + (ci1 * f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 + (((- 1) * f2) + (ci1 * f2))) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()
(c1 + (((- 1) * f2) + (ci1 * f2))) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 + ((- f2) + (ci1 * f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 + ((- f2) + (ci1 * f2))) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 + (- f2)) + (ci1 * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

((c1 + (- f2)) + (ci1 * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

((c1 - f2) + (ci1 * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

((c1 - f2) + (ci1 * f2)) + (- (ci1 * c1)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

((c1 - f2) + (ci1 * f2)) + (ci1 * (- c1)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(ci1 * f2) + (ci1 * (- c1)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 - f2) + ((ci1 * f2) + (ci1 * (- c1))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 - f2) + (ci1 * (f2 + (- c1))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 - f2) + (ci1 * (- (c1 - f2))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(c1 - f2) + (- (ci1 * (c1 - f2))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

- ci1 is real V101() ext-real set

(c1 - f2) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

(1 * (c1 - f2)) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of ()

1 + (- ci1) is real V101() ext-real set