REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V171() non bounded_below non bounded_above interval set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below Element of bool REAL
bool REAL is set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 real-membered pathwise_connected compact SubSpace of R^1
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 real-membered TopStruct
the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct
the carrier of [:I[01],I[01]:] is non empty set
omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below set
bool omega is set
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional finite finite-yielding V29() onto FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V171() set
the empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V29() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() set is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V29() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() set
1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
{{},1} is non empty finite set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 real-membered pathwise_connected compact TopStruct
the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V171() set
[:1,1:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set
bool [:1,1:] is set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is Relation-like complex-yielding ext-real-valued real-valued set
[:[:REAL,REAL:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is set
2 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is set
RealSpace is strict real-membered MetrStruct
[: the carrier of I[01], the carrier of I[01]:] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of I[01], the carrier of I[01]:] is set
bool the carrier of [:I[01],I[01]:] is set
bool NAT is set
COMPLEX is non empty non trivial non finite complex-membered V171() set
bool [:REAL,REAL:] is 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 (TOP-REAL 2) is non empty set
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct
the carrier of [:I[01],I[01]:] is non empty set
[:COMPLEX,COMPLEX:] is Relation-like complex-yielding set
bool [:COMPLEX,COMPLEX:] is set
[:COMPLEX,REAL:] is Relation-like complex-yielding ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is set
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 real-membered pathwise_connected interval SubSpace of R^1
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
bool the carrier of R^1 is set
bool (bool the carrier of R^1) is set
Tunit_circle 2 is non empty TopSpace-like pathwise_connected V202() compact 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 Relation-like set
bool [: the carrier of R^1, the carrier of (Tunit_circle 2):] is set
CircleMap is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued 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 real Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional finite finite-yielding V29() onto V101() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V153() V154() complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() Element of NAT
].0,1.[ is non empty complex-membered ext-real-membered real-membered non left_end non right_end bounded_below bounded_above real-bounded interval Element of bool REAL
R^1 ].0,1.[ is non empty complex-membered ext-real-membered real-membered interval Element of bool the carrier of R^1
R^1 | (R^1 ].0,1.[) is non empty strict TopSpace-like real-membered pathwise_connected interval SubSpace of R^1
the carrier of (R^1 | (R^1 ].0,1.[)) is non empty complex-membered ext-real-membered real-membered set
[: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is 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 real V101() ext-real non negative Element of REAL
3 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
3 / 2 is real V101() ext-real non negative Element of REAL
].(1 / 2),(3 / 2).[ is non empty complex-membered ext-real-membered real-membered non left_end non right_end bounded_below bounded_above real-bounded interval Element of bool 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 (Topen_unit_circle c[-10]), 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 (Topen_unit_circle c[-10]), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is set
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:RAT,RAT:] is Relation-like RAT -valued complex-yielding ext-real-valued real-valued set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued complex-yielding ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] 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())
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty complex-membered ext-real-membered real-membered set
bool the carrier of (TOP-REAL 2) is set
K743(0,1) is real V101() ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
K744(0,1) is real V101() ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
bool the carrier of R^1 is set
[.0,1.] is complex-membered ext-real-membered real-membered interval Element of bool REAL
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
5 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
bool the carrier of I[01] is set
Seg 1 is non empty finite V32(1) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
K745(0,1,K743(0,1),K744(0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):] is set
id (Closed-Interval-TSpace (0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like one-to-one total quasi_total onto bijective continuous V100( Closed-Interval-TSpace (0,1), Closed-Interval-TSpace (0,1)) complex-yielding ext-real-valued real-valued being_homeomorphism Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]
id the carrier of (Closed-Interval-TSpace (0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -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 (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]
K746(0,1,K743(0,1),K744(0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]
n is TopSpace-like TopStruct
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
the_value_of x is set
g is set
x . g is set
{(the_value_of x)} is non empty trivial finite set
(dom x) --> (the_value_of x) is Relation-like dom x -defined {(the_value_of x)} -valued Function-like constant total quasi_total Element of bool [:(dom x),{(the_value_of x)}:]
[:(dom x),{(the_value_of x)}:] is Relation-like set
bool [:(dom x),{(the_value_of 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 (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]
(id (Closed-Interval-TSpace (0,1))) * (id (Closed-Interval-TSpace (0,1))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued the carrier of (Closed-Interval-TSpace (0,1)) -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 (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]
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
Closed-Interval-TSpace (g,C) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,C)) is non empty complex-membered ext-real-membered real-membered set
Closed-Interval-TSpace (x,f) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (x,f)) is non empty complex-membered ext-real-membered real-membered set
Closed-Interval-TSpace (n,r) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (n,r)) 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 (Closed-Interval-TSpace (g,C)) -defined the carrier of (Closed-Interval-TSpace (n,r)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (n,r)):]
[: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (n,r)):] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (n,r)):] is set
L[01] (n,r,x,f) is non empty Relation-like the carrier of (Closed-Interval-TSpace (n,r)) -defined the carrier of (Closed-Interval-TSpace (x,f)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (n,r)), the carrier of (Closed-Interval-TSpace (x,f)):]
[: the carrier of (Closed-Interval-TSpace (n,r)), the carrier of (Closed-Interval-TSpace (x,f)):] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (Closed-Interval-TSpace (n,r)), the carrier of (Closed-Interval-TSpace (x,f)):] is set
(L[01] (n,r,x,f)) * (L[01] (g,C,n,r)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (g,C)) -defined the carrier of (Closed-Interval-TSpace (x,f)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):]
[: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):] is Relation-like complex-yielding ext-real-valued real-valued set
bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):] is set
L[01] (g,C,x,f) is non empty Relation-like the carrier of (Closed-Interval-TSpace (g,C)) -defined the carrier of (Closed-Interval-TSpace (x,f)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):]
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 (Closed-Interval-TSpace (g,C))
bool the carrier of (Closed-Interval-TSpace (g,C)) is set
[#] (Closed-Interval-TSpace (g,C)) is non empty non proper closed complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (g,C))
dom (L[01] (g,C,x,f)) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (g,C))
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
[.g,C.] is complex-membered ext-real-membered real-membered interval Element of bool REAL
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
[#] (Closed-Interval-TSpace (n,r)) is non empty non proper closed complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (n,r))
bool the carrier of (Closed-Interval-TSpace (n,r)) 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 (Closed-Interval-TSpace (g,C))
c is real V101() ext-real set
[.n,r.] is complex-membered ext-real-membered real-membered interval Element of bool REAL
(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 (TOP-REAL n) is non empty set
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
r is Relation-like Function-like set
dom r is set
r .: (n -tuples_on REAL) is set
x is set
n + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
0 + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Seg n is non empty finite V32(n) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
f is set
r . f is set
g is Relation-like NAT -defined REAL -valued Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL
g . 1 is real V101() ext-real set
Funcs ((Seg n),REAL) is non empty functional FUNCTION_DOMAIN of Seg n, REAL
rng g is finite complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of bool REAL
C is Relation-like Function-like set
dom C is set
rng C is set
{x} is non empty trivial finite set
(Seg n) --> x is non empty Relation-like Seg n -defined Seg n -defined {x} -valued Function-like constant finite total total quasi_total FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{x}:]
[:(Seg n),{x}:] is Relation-like finite set
bool [:(Seg n),{x}:] is finite V29() set
dom ((Seg n) --> x) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
rng ((Seg n) --> x) is non empty trivial finite Element of bool {x}
bool {x} is finite V29() set
g is Relation-like NAT -defined REAL -valued Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL
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
[#] (TOP-REAL n) is non empty non proper closed Element of bool the carrier of (TOP-REAL n)
the carrier of (TOP-REAL n) is non empty non trivial non finite set
bool the carrier of (TOP-REAL n) is set
g is non empty a_neighborhood of f
r | g is non empty strict TopSpace-like SubSpace of r
(TOP-REAL n) | ([#] (TOP-REAL n)) is non empty strict TopSpace-like SubSpace of TOP-REAL n
the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))) is non empty set
the carrier of (r | g) is non empty set
[: the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))), the carrier of (r | g):] is Relation-like set
bool [: the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))), the carrier of (r | g):] is set
C is non empty Relation-like the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))) -defined the carrier of (r | g) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))), the carrier of (r | g):]
dom C is non empty Element of bool the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n)))
bool the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))) is set
[#] ((TOP-REAL n) | ([#] (TOP-REAL n))) is non empty non proper closed Element of bool the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n)))
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)
n is ordinal natural real V101() ext-real 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 (TOP-REAL n) is non empty set
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) V45( TOP-REAL n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) 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 (TOP-REAL n)
Sphere ((0. (TOP-REAL n)),1) is closed Element of bool the carrier of (TOP-REAL n)
bool the carrier of (TOP-REAL n) is set
r 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 (TOP-REAL n)
- r 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 (TOP-REAL n)
- r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
{r} is non empty trivial functional finite V29() set
(Sphere ((0. (TOP-REAL n)),1)) \ {r} is Element of bool the carrier of (TOP-REAL n)
x is ordinal natural real V101() ext-real non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
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 (TOP-REAL x) is non empty set
f is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
0. (TOP-REAL x) is Relation-like NAT -defined Function-like finite V32(x) V45( TOP-REAL x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
the ZeroF of (TOP-REAL x) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
f - (0. (TOP-REAL x)) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
f - (0. (TOP-REAL x)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.(f - (0. (TOP-REAL x))).| is real V101() ext-real non negative Element of REAL
- (0. (TOP-REAL x)) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
- (0. (TOP-REAL x)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
f + (- (0. (TOP-REAL x))) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
f + (- (0. (TOP-REAL x))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.(f + (- (0. (TOP-REAL x)))).| is real V101() ext-real non negative Element of REAL
- 1 is real V101() ext-real non positive set
(- 1) * (0. (TOP-REAL n)) 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 (TOP-REAL n)
(- 1) * (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r + ((- 1) * (0. (TOP-REAL n))) 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 (TOP-REAL n)
r + ((- 1) * (0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.(r + ((- 1) * (0. (TOP-REAL n)))).| is real V101() ext-real non negative Element of REAL
r + (0. (TOP-REAL n)) 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 (TOP-REAL n)
r + (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.(r + (0. (TOP-REAL n))).| is real V101() ext-real non negative Element of REAL
|.r.| is real V101() ext-real non negative Element of REAL
|.(0. (TOP-REAL n)).| is real V101() ext-real non negative Element of REAL
1 + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(1 + 1) * r 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 (TOP-REAL n)
(1 + 1) * r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
g is real V101() ext-real set
g * r 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 (TOP-REAL n)
g * r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(g * r) + (g * r) 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 (TOP-REAL n)
(g * r) + (g * r) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(g * r) + r 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 (TOP-REAL n)
(g * r) + r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r + r 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 (TOP-REAL n)
r + r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
r + (- r) 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 (TOP-REAL n)
r + (- r) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.(- r).| is real V101() ext-real non negative Element of REAL
(- r) + (0. (TOP-REAL n)) 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 (TOP-REAL n)
(- r) + (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.((- r) + (0. (TOP-REAL n))).| is real V101() ext-real non negative Element of REAL
(- r) + ((- 1) * (0. (TOP-REAL n))) 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 (TOP-REAL n)
(- r) + ((- 1) * (0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.((- r) + ((- 1) * (0. (TOP-REAL n)))).| is real V101() ext-real non negative Element of REAL
- (0. (TOP-REAL n)) 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 (TOP-REAL n)
- (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- r) + (- (0. (TOP-REAL n))) 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 (TOP-REAL n)
(- r) + (- (0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.((- r) + (- (0. (TOP-REAL n)))).| is real V101() ext-real non negative Element of REAL
- f is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
- f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- f) - (0. (TOP-REAL x)) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)
(- f) - (0. (TOP-REAL x)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|.((- f) - (0. (TOP-REAL x))).| is real V101() ext-real non negative Element of REAL
Sphere ((0. (TOP-REAL x)),1) is closed bounded Element of bool the carrier of (TOP-REAL x)
bool the carrier of (TOP-REAL x) 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
dom f is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of I[01]
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
x is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total continuous Path of r,r
f is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total continuous Path of r,r
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 [:I[01],I[01]:], the carrier of r:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of r:] is set
V is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of r -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of r:]
[: the carrier of [:I[01],I[01]:], the carrier of n:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of n:] is set
c is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], 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))
n is non empty trivial finite 1 -element TopSpace-like pathwise_connected TopStruct
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 [:(Loops r),(Loops r):]
[:(Loops r),(Loops r):] is Relation-like set
bool [:(Loops r),(Loops r):] 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 (Loops r)
bool (Loops r) 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 (Loops r)
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
n is ordinal natural real V101() ext-real 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 (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is set
[#] (TOP-REAL n) is non empty non proper closed Element of bool the carrier of (TOP-REAL n)
r 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 (TOP-REAL n)
{r} is non empty trivial functional finite V29() set
([#] (TOP-REAL n)) \ {r} is Element of bool the carrier of (TOP-REAL n)
x is Element of bool the carrier of (TOP-REAL n)
(TOP-REAL n) | x is strict TopSpace-like SubSpace of TOP-REAL n
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
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 (TOP-REAL n)
x 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 (TOP-REAL n)
LSeg (f2,x) is Element of bool the carrier of (TOP-REAL n)
(TOP-REAL n) | (LSeg (f2,x)) is strict TopSpace-like SubSpace of TOP-REAL n
[#] ((TOP-REAL n) | (LSeg (f2,x))) is non proper closed Element of bool the carrier of ((TOP-REAL n) | (LSeg (f2,x)))
the carrier of ((TOP-REAL n) | (LSeg (f2,x))) is set
bool the carrier of ((TOP-REAL n) | (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
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 (TOP-REAL n)
x 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 (TOP-REAL n)
LSeg (f2,x) is Element of bool the carrier of (TOP-REAL n)
p is ordinal natural real V101() ext-real non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
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 (TOP-REAL p) is non empty set
U 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 (TOP-REAL p)
V 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 (TOP-REAL p)
c is real V101() ext-real Element of REAL
1 - c is real V101() ext-real set
(1 - c) * U 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 (TOP-REAL p)
(1 - c) * U is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
c * V 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 (TOP-REAL p)
c * V is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((1 - c) * U) + (c * V) 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 (TOP-REAL p)
((1 - c) * U) + (c * V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
x - 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 (TOP-REAL n)
x - f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
n - 1 is real V101() ext-real set
fc2 is ordinal natural real V101() ext-real non negative set
fc2 + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
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 (TOP-REAL n)
(TOP-REAL n) | (Plane ((x - f2),r)) is strict TopSpace-like SubSpace of TOP-REAL n
[#] ((TOP-REAL n) | (Plane ((x - f2),r))) is non proper closed Element of bool the carrier of ((TOP-REAL n) | (Plane ((x - f2),r)))
the carrier of ((TOP-REAL n) | (Plane ((x - f2),r))) is set
bool the carrier of ((TOP-REAL n) | (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 (TOP-REAL n) : |((x - f2),(b1 - r))| = 0 } is set
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 (TOP-REAL n)
c1 - r 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 (TOP-REAL n)
c1 - r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
|((x - f2),(c1 - r))| is real V101() ext-real Element of REAL
|((x - f2),(x - f2))| is real V101() ext-real Element of REAL
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) V45( TOP-REAL n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) 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 (TOP-REAL n)
LSeg (f2,c1) is Element of bool the carrier of (TOP-REAL n)
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 (TOP-REAL p)
ci1 is real V101() ext-real Element of REAL
1 - ci1 is real V101() ext-real set
(1 - ci1) * U 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 (TOP-REAL p)
(1 - ci1) * U is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
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 (TOP-REAL p)
ci1 * c2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((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 (TOP-REAL p)
((1 - ci1) * U) + (ci1 * c2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) V45( TOP-REAL n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) 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 (TOP-REAL n)
1 * 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 (TOP-REAL n)
1 * 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
(0. (TOP-REAL n)) + (1 * 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 (TOP-REAL n)
(0. (TOP-REAL n)) + (1 * 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
(0. (TOP-REAL n)) + 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 (TOP-REAL n)
(0. (TOP-REAL n)) + 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 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 (TOP-REAL n)
c1 - f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(1 - 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 (TOP-REAL n)
(1 - ci1) * f2 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 - ((1 - 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 (TOP-REAL n)
c1 - ((1 - ci1) * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
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 (TOP-REAL n)
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 - ((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 (TOP-REAL n)
(c1 - ((1 - 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
- ((1 - 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 (TOP-REAL n)
- ((1 - ci1) * f2) 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 + (- ((1 - 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 (TOP-REAL n)
c1 + (- ((1 - ci1) * f2)) 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 + (- ((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 (TOP-REAL n)
(c1 + (- ((1 - 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
- (1 - ci1) is real V101() ext-real set
(- (1 - 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 (TOP-REAL n)
(- (1 - ci1)) * f2 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 + ((- (1 - 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 (TOP-REAL n)
c1 + ((- (1 - ci1)) * f2) 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 + ((- (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 (TOP-REAL n)
(c1 + ((- (1 - 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
- 1 is real V101() ext-real non positive set
(- 1) + ci1 is real V101() ext-real set
((- 1) + 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 (TOP-REAL n)
((- 1) + ci1) * f2 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 + (((- 1) + 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 (TOP-REAL n)
c1 + (((- 1) + ci1) * f2) 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 + (((- 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 (TOP-REAL n)
(c1 + (((- 1) + 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
(- 1) * 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 (TOP-REAL n)
(- 1) * f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
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 (TOP-REAL n)
ci1 * f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
((- 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 (TOP-REAL n)
((- 1) * f2) + (ci1 * f2) 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 + (((- 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 (TOP-REAL n)
c1 + (((- 1) * f2) + (ci1 * f2)) 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 + (((- 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 (TOP-REAL n)
(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
- 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 (TOP-REAL n)
- f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(- 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 (TOP-REAL n)
(- f2) + (ci1 * f2) 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 (TOP-REAL n)
c1 + ((- f2) + (ci1 * f2)) 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))) - (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 (TOP-REAL n)
(c1 + ((- 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) 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 (TOP-REAL n)
c1 + (- f2) 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 (TOP-REAL n)
(c1 + (- f2)) + (ci1 * f2) 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)) - (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 (TOP-REAL n)
((c1 + (- 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 (TOP-REAL n)
(c1 - f2) + (ci1 * f2) 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)) - (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 (TOP-REAL n)
((c1 - 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
- (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 (TOP-REAL n)
- (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)) + (- (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 (TOP-REAL n)
((c1 - 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 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 (TOP-REAL n)
- 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
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 (TOP-REAL n)
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)) + (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 (TOP-REAL n)
((c1 - 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
(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 (TOP-REAL n)
(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) + (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 (TOP-REAL n)
(c1 - 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
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 (TOP-REAL n)
f2 + (- 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
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 (TOP-REAL n)
ci1 * (f2 + (- 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 + (- 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 (TOP-REAL n)
(c1 - f2) + (ci1 * (f2 + (- 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) 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 (TOP-REAL n)
- (c1 - f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
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 (TOP-REAL n)
ci1 * (- (c1 - f2)) 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 * (- (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 (TOP-REAL n)
(c1 - f2) + (ci1 * (- (c1 - f2))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
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 (TOP-REAL n)
ci1 * (c1 - f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- (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 (TOP-REAL n)
- (ci1 * (c1 - f2)) 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 * (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 (TOP-REAL n)
(c1 - f2) + (- (ci1 * (c1 - f2))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
- ci1 is real V101() ext-real set
(- 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 (TOP-REAL n)
(- ci1) * (c1 - f2) 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) * (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 (TOP-REAL n)
(c1 - f2) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
1 * (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 (TOP-REAL n)
1 * (c1 - f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
(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 (TOP-REAL n)
(1 * (c1 - f2)) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL
1 + (- ci1) is real V101() ext-real set
(1 + (- 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 (TOP-REAL n)