REAL is non empty V32() V62() V63() V64() V68() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V62() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
K19(REAL) is V32() set
omega is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V62() V63() V64() V65() V66() V67() V68() set
K19(omega) is V32() set
K19(NAT) is V32() set
INT is non empty V32() V62() V63() V64() V65() V66() V68() set
K95(NAT) is V24() set
COMPLEX is non empty V32() V62() V68() set
RAT is non empty V32() V62() V63() V64() V65() V68() set
K20(COMPLEX,COMPLEX) is Relation-like V32() complex-valued set
K19(K20(COMPLEX,COMPLEX)) is V32() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V32() complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V32() set
K20(REAL,REAL) is Relation-like V32() complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is V32() set
K20(K20(REAL,REAL),REAL) is Relation-like V32() complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is V32() set
K20(RAT,RAT) is Relation-like RAT -valued V32() complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is V32() set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V32() complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is V32() set
K20(INT,INT) is Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is V32() set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is V32() set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is V32() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
{{},1} is non empty V62() V63() V64() V65() V66() V67() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer V47() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of NAT
Seg 1 is non empty V12() V32() V39(1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() set
Seg 2 is non empty V32() V39(2) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty V62() V63() V64() V65() V66() V67() set
addcomplex is Relation-like Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) having_a_unity complex-valued commutative associative Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() FinSequence of REAL
Sum (<*> REAL) is V43() real ext-real Element of REAL
multcomplex is Relation-like Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) having_a_unity complex-valued commutative associative Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
Product (<*> REAL) is V43() real ext-real Element of REAL
the_unity_wrt addcomplex is V43() Element of COMPLEX
the_unity_wrt multcomplex is V43() Element of COMPLEX
- 1 is V43() real integer ext-real non positive set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
rng u is V62() V63() V64() V65() V66() Element of K19(REAL)
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
u | m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
Seg m is V32() V39(m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
u | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined Function-like FinSubsequence-like complex-valued set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u | m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
Seg m is V32() V39(m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
u | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u /^ m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
rng u is V62() V63() V64() V65() V66() Element of K19(REAL)
c is set
rng (u /^ m) is set
dom (u /^ m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
s is set
(u /^ m) . s is set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i + i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i + m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . (i + m) is V43() real integer ext-real set
(u /^ m) . i is set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is V43() real integer ext-real set
<*u*> is Relation-like NAT -defined Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,u] is set
{[1,u]} is Relation-like Function-like constant non empty V12() V39(1) set
{u} is non empty V12() V39(1) V62() V63() V64() V65() V66() set
m is set
rng <*u*> is non empty V12() V39(1) V62() V63() V64() Element of K19(REAL)
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u ^ m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
rng (u ^ m) is V62() V63() V64() Element of K19(REAL)
rng u is V62() V63() V64() V65() V66() Element of K19(REAL)
rng m is V62() V63() V64() V65() V66() Element of K19(REAL)
(rng u) \/ (rng m) is V62() V63() V64() V65() V66() Element of K19(REAL)
z is set
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
u + m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len (u + m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
min ((len u),(len m)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg c is V32() V39(c) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= c ) } is set
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
dom (u + m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(dom u) /\ (dom m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
min (c,i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
min (c,i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
u - m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len (u - m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
min ((len u),(len m)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg c is V32() V39(c) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= c ) } is set
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
dom (u - m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(dom u) /\ (dom m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
min (c,i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
min (c,i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
u (#) m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len (u (#) m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
min ((len u),(len m)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg c is V32() V39(c) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= c ) } is set
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
dom (u (#) m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(dom u) /\ (dom m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
min (c,i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
min (c,i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u + m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len (u + m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
min ((len u),(len m)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u - m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len (u - m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
min ((len u),(len m)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u (#) m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len (u (#) m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
min ((len u),(len m)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u (#) m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(u (#) m) | z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
Seg z is V32() V39(z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= z ) } is set
(u (#) m) | (Seg z) is Relation-like NAT -defined Seg z -defined NAT -defined Function-like FinSubsequence-like complex-valued set
u | z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
u | (Seg z) is Relation-like NAT -defined Seg z -defined NAT -defined Function-like FinSubsequence-like complex-valued set
m | z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
m | (Seg z) is Relation-like NAT -defined Seg z -defined NAT -defined Function-like FinSubsequence-like complex-valued set
(u | z) (#) (m | z) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len (u | z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (u (#) m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u (#) m) | z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (m | z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u | z) (#) (m | z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg s is V32() V39(s) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= s ) } is set
u | s is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
u | (Seg s) is Relation-like NAT -defined Seg s -defined NAT -defined Function-like FinSubsequence-like complex-valued set
dom (u | s) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom ((u | z) (#) (m | z)) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
m | s is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
m | (Seg s) is Relation-like NAT -defined Seg s -defined NAT -defined Function-like FinSubsequence-like complex-valued set
dom (m | s) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len (u (#) m)) is V32() V39( len (u (#) m)) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len (u (#) m) ) } is set
dom (u (#) m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom ((u (#) m) | z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
((u (#) m) | z) . i is V43() set
(u (#) m) . i is V43() set
u . i is V43() set
m . i is V43() set
(u . i) * (m . i) is set
(u | s) . i is V43() set
((u | s) . i) * (m . i) is set
(m | s) . i is V43() set
((u | s) . i) * ((m | s) . i) is set
((u | z) (#) (m | z)) . i is V43() set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum u is V43() real ext-real set
z is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex $$ z is V43() Element of COMPLEX
[#] (z,(the_unity_wrt addcomplex)) is Relation-like Function-like V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
K20(NAT,COMPLEX) is Relation-like V32() complex-valued set
K19(K20(NAT,COMPLEX)) is V32() set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
finSeg i is V32() V39(i) Element of K95(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
addcomplex $$ ((finSeg i),([#] (z,(the_unity_wrt addcomplex)))) is V43() Element of COMPLEX
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
finSeg (i + 1) is non empty V32() V39(i + 1) Element of K95(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i + 1 ) } is set
addcomplex $$ ((finSeg (i + 1)),([#] (z,(the_unity_wrt addcomplex)))) is V43() Element of COMPLEX
([#] (z,(the_unity_wrt addcomplex))) . (i + 1) is V43() Element of COMPLEX
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z . (i + 1) is V43() set
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{.(i + 1).} is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() Element of K95(NAT)
(finSeg i) \/ {.(i + 1).} is non empty Element of K95(NAT)
addcomplex $$ (((finSeg i) \/ {.(i + 1).}),([#] (z,(the_unity_wrt addcomplex)))) is V43() Element of COMPLEX
addcomplex . ((addcomplex $$ ((finSeg i),([#] (z,(the_unity_wrt addcomplex))))),(([#] (z,(the_unity_wrt addcomplex))) . (i + 1))) is V43() Element of COMPLEX
i is V43() real integer ext-real set
s is V43() real integer ext-real set
i + s is V43() real integer ext-real set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( 0 ) V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
{}. NAT is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K95(NAT)
finSeg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( 0 ) V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K95(NAT)
addcomplex $$ ((finSeg 0),([#] (z,(the_unity_wrt addcomplex)))) is V43() Element of COMPLEX
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
findom z is V62() V63() V64() V65() V66() V67() Element of K95(NAT)
addcomplex $$ ((findom z),([#] (z,(the_unity_wrt addcomplex)))) is V43() Element of COMPLEX
Product u is V43() real ext-real set
z is Relation-like NAT -defined COMPLEX -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
multcomplex $$ z is V43() Element of COMPLEX
[#] (z,(the_unity_wrt multcomplex)) is Relation-like Function-like V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
K20(NAT,COMPLEX) is Relation-like V32() complex-valued set
K19(K20(NAT,COMPLEX)) is V32() set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
finSeg i is V32() V39(i) Element of K95(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
multcomplex $$ ((finSeg i),([#] (z,(the_unity_wrt multcomplex)))) is V43() Element of COMPLEX
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
finSeg (i + 1) is non empty V32() V39(i + 1) Element of K95(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i + 1 ) } is set
multcomplex $$ ((finSeg (i + 1)),([#] (z,(the_unity_wrt multcomplex)))) is V43() Element of COMPLEX
([#] (z,(the_unity_wrt multcomplex))) . (i + 1) is V43() Element of COMPLEX
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z . (i + 1) is V43() set
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{.(i + 1).} is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() Element of K95(NAT)
(finSeg i) \/ {.(i + 1).} is non empty Element of K95(NAT)
multcomplex $$ (((finSeg i) \/ {.(i + 1).}),([#] (z,(the_unity_wrt multcomplex)))) is V43() Element of COMPLEX
multcomplex . ((multcomplex $$ ((finSeg i),([#] (z,(the_unity_wrt multcomplex))))),(([#] (z,(the_unity_wrt multcomplex))) . (i + 1))) is V43() Element of COMPLEX
i is V43() real integer ext-real set
s is V43() real integer ext-real set
i * s is V43() real integer ext-real set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( 0 ) V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
{}. NAT is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K95(NAT)
finSeg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( 0 ) V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K95(NAT)
multcomplex $$ ((finSeg 0),([#] (z,(the_unity_wrt multcomplex)))) is V43() Element of COMPLEX
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
findom z is V62() V63() V64() V65() V66() V67() Element of K95(NAT)
multcomplex $$ ((findom z),([#] (z,(the_unity_wrt multcomplex)))) is V43() Element of COMPLEX
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
rng u is V62() V63() V64() V65() V66() Element of K19(REAL)
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
u | m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
Seg m is V32() V39(m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
u | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined Function-like FinSubsequence-like complex-valued set
u . (m + 1) is V43() set
<*(u . (m + 1))*> is Relation-like NAT -defined Function-like constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued set
[1,(u . (m + 1))] is set
{[1,(u . (m + 1))]} is Relation-like Function-like constant non empty V12() V39(1) set
(u | m) ^ <*(u . (m + 1))*> is Relation-like NAT -defined Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued set
u | (m + 1) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
Seg (m + 1) is non empty V32() V39(m + 1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m + 1 ) } is set
u | (Seg (m + 1)) is Relation-like NAT -defined Seg (m + 1) -defined NAT -defined Function-like FinSubsequence-like complex-valued set
i is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (u | m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len <*(u . (m + 1))*> is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
(len (u | m)) + (len <*(u . (m + 1))*>) is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
(len (u | m)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (u | (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom i is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len (u | (m + 1))) is V32() V39( len (u | (m + 1))) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len (u | (m + 1)) ) } is set
dom (u | (m + 1)) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
s is set
Seg (len i) is V32() V39( len i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len i ) } is set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom <*(u . (m + 1))*> is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i . s is V43() set
<*(u . (m + 1))*> . 1 is V43() set
(u | (m + 1)) . s is V43() set
dom (u | m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i . s is V43() set
(u | m) . i is V43() set
u . i is V43() set
(u | (m + 1)) . s is V43() set
u is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product u is V43() set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
z | m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
Seg m is V32() V39(m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
z | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined Function-like FinSubsequence-like complex-valued set
len z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (z | m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
z . (m + 1) is V43() set
<*(z . (m + 1))*> is Relation-like NAT -defined Function-like constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued set
[1,(z . (m + 1))] is set
{[1,(z . (m + 1))]} is Relation-like Function-like constant non empty V12() V39(1) set
i ^ <*(z . (m + 1))*> is Relation-like NAT -defined Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued set
Product z is V43() set
Product i is V43() set
(Product i) * (z . (m + 1)) is set
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z . s is V43() set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z . s is V43() set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len z) is V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
dom i is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i . i is V43() set
z . i is V43() set
z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z . c is V43() set
Product z is V43() set
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product m is V43() set
Seg (len m) is V32() V39( len m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len m ) } is set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m . z is V43() set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . m is V43() set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m is V43() real integer ext-real set
z is V43() real integer ext-real set
m - z is V43() real integer ext-real set
- z is V43() real integer ext-real set
m + (- z) is V43() real integer ext-real set
u is V43() real integer ext-real set
(m - z) mod u is V43() real integer ext-real set
m mod u is V43() real integer ext-real set
z mod u is V43() real integer ext-real set
(m mod u) - (z mod u) is V43() real integer ext-real set
- (z mod u) is V43() real integer ext-real set
(m mod u) + (- (z mod u)) is V43() real integer ext-real set
((m mod u) - (z mod u)) mod u is V43() real integer ext-real set
z div u is V43() real integer ext-real set
(z div u) * u is V43() real integer ext-real set
(z mod u) + ((z div u) * u) is V43() real integer ext-real set
z - ((z div u) * u) is V43() real integer ext-real set
- ((z div u) * u) is V43() real integer ext-real set
z + (- ((z div u) * u)) is V43() real integer ext-real set
(z - ((z div u) * u)) + ((z div u) * u) is V43() real integer ext-real set
m div u is V43() real integer ext-real set
(m div u) * u is V43() real integer ext-real set
(m mod u) + ((m div u) * u) is V43() real integer ext-real set
m - ((m div u) * u) is V43() real integer ext-real set
- ((m div u) * u) is V43() real integer ext-real set
m + (- ((m div u) * u)) is V43() real integer ext-real set
(m - ((m div u) * u)) + ((m div u) * u) is V43() real integer ext-real set
(m - z) - ((m mod u) - (z mod u)) is V43() real integer ext-real set
- ((m mod u) - (z mod u)) is V43() real integer ext-real set
(m - z) + (- ((m mod u) - (z mod u))) is V43() real integer ext-real set
(m div u) - (z div u) is V43() real integer ext-real set
- (z div u) is V43() real integer ext-real set
(m div u) + (- (z div u)) is V43() real integer ext-real set
((m div u) - (z div u)) * u is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
z is V43() real integer ext-real set
z * u is V43() real integer ext-real set
z * m is V43() real integer ext-real set
c is V43() real integer ext-real set
u * c is V43() real integer ext-real set
u * z is V43() real integer ext-real set
(u * z) * c is V43() real integer ext-real set
m * z is V43() real integer ext-real set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product u is V43() real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . m is V43() real integer ext-real set
(Product u) / (u . m) is V43() real ext-real set
(u . m) " is V43() real ext-real set
(Product u) * ((u . m) ") is V43() real ext-real set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u /^ z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u | z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg z is V32() V39(z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= z ) } is set
u | (Seg z) is Relation-like NAT -defined Seg z -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len u) is V32() V39( len u) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len u ) } is set
1 - 1 is V43() real integer ext-real set
1 + (- 1) is V43() real integer ext-real set
z - 1 is V43() real integer ext-real set
z + (- 1) is V43() real integer ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
u | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u | i) ^ (u /^ z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
c is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
i ^ c is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . z is V43() real integer ext-real set
<*(u . z)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(u . z)] is set
{[1,(u . z)]} is Relation-like Function-like constant non empty V12() V39(1) set
(u | i) ^ <*(u . z)*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product ((u | i) ^ <*(u . z)*>) is V43() real integer ext-real set
Product (u /^ z) is V43() real integer ext-real set
(Product ((u | i) ^ <*(u . z)*>)) * (Product (u /^ z)) is V43() real integer ext-real set
Product (u | i) is V43() real integer ext-real set
Product <*(u . z)*> is V43() real integer ext-real set
(Product (u | i)) * (Product <*(u . z)*>) is V43() real integer ext-real set
((Product (u | i)) * (Product <*(u . z)*>)) * (Product (u /^ z)) is V43() real integer ext-real set
(Product (u | i)) * (Product (u /^ z)) is V43() real integer ext-real set
((Product (u | i)) * (Product (u /^ z))) * (Product <*(u . z)*>) is V43() real integer ext-real set
((Product (u | i)) * (Product (u /^ z))) * (u . z) is V43() real integer ext-real set
cc is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
Product cc is V43() real integer ext-real set
(Product cc) * (u . z) is V43() real integer ext-real set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product u is V43() real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . m is V43() real integer ext-real set
(Product u) / (u . m) is V43() real ext-real set
(u . m) " is V43() real ext-real set
(Product u) * ((u . m) ") is V43() real ext-real set
z is V43() real integer ext-real set
z * (u . m) is V43() real integer ext-real set
((u . m) ") * (u . m) is V43() real ext-real set
(Product u) * (((u . m) ") * (u . m)) is V43() real ext-real set
(Product u) * 1 is V43() real integer ext-real set
1 * (u . m) is V43() real integer ext-real set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product u is V43() real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . z is V43() real integer ext-real set
u . m is V43() real integer ext-real set
(Product u) / (u . z) is V43() real ext-real set
(u . z) " is V43() real ext-real set
(Product u) * ((u . z) ") is V43() real ext-real set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len u) is V32() V39( len u) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len u ) } is set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
1 - 1 is V43() real integer ext-real set
1 + (- 1) is V43() real integer ext-real set
s - 1 is V43() real integer ext-real set
s + (- 1) is V43() real integer ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
u | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u /^ s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u | i) ^ (u /^ s) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (u | i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i - 1 is V43() real integer ext-real set
i + (- 1) is V43() real integer ext-real set
cc is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
dom cc is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
u . i is V43() real integer ext-real set
dom (u | i) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u | i) . i is V43() real integer ext-real set
cc . i is V43() real integer ext-real set
(i - 1) - i is V43() real integer ext-real set
- i is V43() real integer ext-real non positive set
(i - 1) + (- i) is V43() real integer ext-real set
i - i is V43() real integer ext-real set
i + (- i) is V43() real integer ext-real set
(i + 1) - i is V43() real integer ext-real set
(i + 1) + (- i) is V43() real integer ext-real set
(i - i) - 1 is V43() real integer ext-real set
(i - i) + (- 1) is V43() real integer ext-real set
b is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (u /^ s) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
(len u) - s is V43() real integer ext-real set
- s is V43() real integer ext-real non positive set
(len u) + (- s) is V43() real integer ext-real set
len cc is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i + ((len u) - s) is V43() real integer ext-real set
(len u) - 1 is V43() real integer ext-real set
(len u) + (- 1) is V43() real integer ext-real set
a is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i - s is V43() real integer ext-real set
i + (- s) is V43() real integer ext-real set
Seg (len (u /^ s)) is V32() V39( len (u /^ s)) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len (u /^ s) ) } is set
c is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
c /^ s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
dom (c /^ s) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len cc) is V32() V39( len cc) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len cc ) } is set
r is set
cc . a is V43() real integer ext-real set
a - i is V43() real integer ext-real set
a + (- i) is V43() real integer ext-real set
(u /^ s) . (a - i) is V43() real integer ext-real set
s is Relation-like NAT -defined r -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r
s /^ s is Relation-like NAT -defined r -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of r
(s /^ s) /. (a - i) is Element of r
s + b is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
s /. (s + b) is Element of r
b is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
cc . b is V43() real integer ext-real set
b is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
cc . b is V43() real integer ext-real set
len cc is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len cc) is V32() V39( len cc) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len cc ) } is set
b - 1 is V43() real integer ext-real set
b + (- 1) is V43() real integer ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
cc | r is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
Seg r is V32() V39(r) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
cc | (Seg r) is Relation-like NAT -defined Seg r -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
<*(cc . b)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(cc . b)] is set
{[1,(cc . b)]} is Relation-like Function-like constant non empty V12() V39(1) set
(cc | r) ^ <*(cc . b)*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
cc | b is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
Seg b is V32() V39(b) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= b ) } is set
cc | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
cc /^ b is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
((cc | r) ^ <*(cc . b)*>) ^ (cc /^ b) is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product cc is V43() real integer ext-real set
Product ((cc | r) ^ <*(cc . b)*>) is V43() real integer ext-real set
Product (cc /^ b) is V43() real integer ext-real set
(Product ((cc | r) ^ <*(cc . b)*>)) * (Product (cc /^ b)) is V43() real integer ext-real set
Product (cc | r) is V43() real integer ext-real set
Product <*(cc . b)*> is V43() real integer ext-real set
(Product (cc | r)) * (Product <*(cc . b)*>) is V43() real integer ext-real set
((Product (cc | r)) * (Product <*(cc . b)*>)) * (Product (cc /^ b)) is V43() real integer ext-real set
(Product (cc | r)) * (Product (cc /^ b)) is V43() real integer ext-real set
<*(u . i)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(u . i)] is set
{[1,(u . i)]} is Relation-like Function-like constant non empty V12() V39(1) set
Product <*(u . i)*> is V43() real integer ext-real set
((Product (cc | r)) * (Product (cc /^ b))) * (Product <*(u . i)*>) is V43() real integer ext-real set
((Product (cc | r)) * (Product (cc /^ b))) * (u . i) is V43() real integer ext-real set
(cc | r) ^ (cc /^ b) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
Product ((cc | r) ^ (cc /^ b)) is V43() real integer ext-real set
(Product ((cc | r) ^ (cc /^ b))) * (u . i) is V43() real integer ext-real set
u . s is V43() real integer ext-real set
<*(u . s)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(u . s)] is set
{[1,(u . s)]} is Relation-like Function-like constant non empty V12() V39(1) set
(u | i) ^ <*(u . s)*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u | s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg s is V32() V39(s) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= s ) } is set
u | (Seg s) is Relation-like NAT -defined Seg s -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
c is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
p is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
p ^ s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
Product ((u | i) ^ <*(u . s)*>) is V43() real integer ext-real set
Product (u /^ s) is V43() real integer ext-real set
(Product ((u | i) ^ <*(u . s)*>)) * (Product (u /^ s)) is V43() real integer ext-real set
Product (u | i) is V43() real integer ext-real set
Product <*(u . s)*> is V43() real integer ext-real set
(Product (u | i)) * (Product <*(u . s)*>) is V43() real integer ext-real set
((Product (u | i)) * (Product <*(u . s)*>)) * (Product (u /^ s)) is V43() real integer ext-real set
(Product (u | i)) * (Product (u /^ s)) is V43() real integer ext-real set
((Product (u | i)) * (Product (u /^ s))) * (Product <*(u . s)*>) is V43() real integer ext-real set
((Product (u | i)) * (Product (u /^ s))) * (u . s) is V43() real integer ext-real set
(Product cc) * (u . s) is V43() real integer ext-real set
(Product u) / (u . s) is V43() real ext-real set
(u . s) " is V43() real ext-real set
(Product u) * ((u . s) ") is V43() real ext-real set
(u . s) * ((u . s) ") is V43() real ext-real set
(Product cc) * ((u . s) * ((u . s) ")) is V43() real ext-real set
(Product cc) * 1 is V43() real integer ext-real set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product u is V43() real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . z is V43() real integer ext-real set
u . m is V43() real integer ext-real set
(u . m) * (u . z) is V43() real integer ext-real set
(Product u) / ((u . m) * (u . z)) is V43() real ext-real set
((u . m) * (u . z)) " is V43() real ext-real set
(Product u) * (((u . m) * (u . z)) ") is V43() real ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . c is V43() real integer ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . i is V43() real integer ext-real set
(Product u) / (u . i) is V43() real ext-real set
(u . i) " is V43() real ext-real set
(Product u) * ((u . i) ") is V43() real ext-real set
s is V43() real integer ext-real set
s / (u . c) is V43() real ext-real set
(u . c) " is V43() real ext-real set
s * ((u . c) ") is V43() real ext-real set
((u . i) ") * ((u . c) ") is V43() real ext-real set
(Product u) * (((u . i) ") * ((u . c) ")) is V43() real ext-real set
(u . c) * (u . i) is V43() real integer ext-real set
(Product u) / ((u . c) * (u . i)) is V43() real ext-real set
((u . c) * (u . i)) " is V43() real ext-real set
(Product u) * (((u . c) * (u . i)) ") is V43() real ext-real set
i is V43() real integer ext-real set
i * (u . c) is V43() real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . z is V43() real integer ext-real set
u . m is V43() real integer ext-real set
Product u is V43() real integer ext-real set
(Product u) / (u . z) is V43() real ext-real set
(u . z) " is V43() real ext-real set
(Product u) * ((u . z) ") is V43() real ext-real set
u is V43() real integer ext-real set
abs u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
- u is V43() real integer ext-real set
u * (- 1) is V43() real integer ext-real set
(abs u) * (- 1) is V43() real integer ext-real non positive set
- u is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u gcd m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
abs m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u gcd (abs m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
c is V43() real integer ext-real set
(u gcd (abs m)) * c is V43() real integer ext-real set
i is V43() real integer ext-real set
(abs m) * i is V43() real integer ext-real set
s is V43() real integer ext-real set
m * s is V43() real integer ext-real set
i is V43() real integer ext-real set
v is V43() real integer ext-real set
i * v is V43() real integer ext-real set
v * s is V43() real integer ext-real set
i * (v * s) is V43() real integer ext-real set
c * i is V43() real integer ext-real set
(u gcd (abs m)) * (c * i) is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u lcm m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u * m is V43() real integer ext-real set
abs (u * m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u gcd m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z is V43() real integer ext-real set
m * z is V43() real integer ext-real set
c is V43() real integer ext-real set
u * c is V43() real integer ext-real set
i is V43() real integer ext-real set
(u lcm m) * i is V43() real integer ext-real set
z * i is V43() real integer ext-real set
m * (z * i) is V43() real integer ext-real set
c * i is V43() real integer ext-real set
u * (c * i) is V43() real integer ext-real set
s is V43() real integer ext-real set
- (u * m) is V43() real integer ext-real set
- (- (u * m)) is V43() real integer ext-real set
abs m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
abs u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
(abs u) * (abs m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u * m is V43() real integer ext-real set
z is V43() real integer ext-real set
u * z is V43() real integer ext-real set
(u * m) gcd (u * z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
abs u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m gcd z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(abs u) * (m gcd z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
0 * (m gcd z) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer V47() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of NAT
u * (m gcd z) is V43() real integer ext-real set
s is V43() real integer ext-real set
(u * (m gcd z)) * s is V43() real integer ext-real set
(m gcd z) * s is V43() real integer ext-real set
i is V43() real integer ext-real set
((u * (m gcd z)) * s) * i is V43() real integer ext-real set
((m gcd z) * s) * i is V43() real integer ext-real set
u * (((m gcd z) * s) * i) is V43() real integer ext-real set
v is V43() real integer ext-real set
((u * (m gcd z)) * s) * v is V43() real integer ext-real set
((m gcd z) * s) * v is V43() real integer ext-real set
u * (((m gcd z) * s) * v) is V43() real integer ext-real set
i is V43() real integer ext-real set
((m gcd z) * s) * i is V43() real integer ext-real set
s * i is V43() real integer ext-real set
(m gcd z) * (s * i) is V43() real integer ext-real set
(m gcd z) * 1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
0 * u is V43() real integer ext-real set
(m gcd z) * u is V43() real integer ext-real set
- u is V43() real integer ext-real set
- (- u) is V43() real integer ext-real set
0 * (- u) is V43() real integer ext-real set
(m gcd z) * (- u) is V43() real integer ext-real set
(- u) * (m gcd z) is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u * m is V43() real integer ext-real set
(u * m) gcd u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
abs u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
z is V43() real integer ext-real set
c is V43() real integer ext-real set
z * c is V43() real integer ext-real set
i is V43() real integer ext-real set
u * i is V43() real integer ext-real set
c * i is V43() real integer ext-real set
z * (c * i) is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
z is V43() real integer ext-real set
m gcd z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u gcd (m gcd z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u gcd m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(u gcd m) gcd z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
- ((u gcd m) gcd z) is V43() real integer ext-real non positive set
(- ((u gcd m) gcd z)) * (- 1) is V43() real integer ext-real non negative set
0 * (- 1) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
z is V43() real integer ext-real set
m * z is V43() real integer ext-real set
u gcd (m * z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u gcd z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u gcd m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u * z is V43() real integer ext-real set
(u * z) gcd (m * z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
abs z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
(abs z) * (u gcd m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u gcd (abs z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u gcd (u * z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(u gcd (u * z)) gcd (m * z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
abs u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
(abs u) gcd (m * z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(m * z) gcd u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u * m is V43() real integer ext-real set
u lcm m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
abs (u * m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
z is V43() real integer ext-real set
(abs (u * m)) * z is V43() real integer ext-real set
z * (u * m) is V43() real integer ext-real set
- z is V43() real integer ext-real set
(- z) * (u * m) is V43() real integer ext-real set
- (u * m) is V43() real integer ext-real set
z * (- (u * m)) is V43() real integer ext-real set
z is V43() real integer ext-real set
c is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
z * c is V43() real integer ext-real set
z lcm c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u - m is V43() real integer ext-real set
- m is V43() real integer ext-real set
u + (- m) is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u gcd m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z is V43() real integer ext-real set
z * u is V43() real integer ext-real set
c is V43() real integer ext-real set
c * m is V43() real integer ext-real set
(z * u) + (c * m) is V43() real integer ext-real set
(z * u) - 1 is V43() real integer ext-real set
(z * u) + (- 1) is V43() real integer ext-real set
- c is V43() real integer ext-real set
(- c) * m is V43() real integer ext-real set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . m is V43() real integer ext-real set
m is set
dom u is V62() V63() V64() V65() V66() V67() set
u . m is V43() real integer ext-real set
<*0*> is Relation-like NAT -defined NAT -valued INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V56() decreasing non-decreasing non-increasing FinSequence of NAT
[1,0] is set
{[1,0]} is Relation-like Function-like constant non empty V12() V39(1) set
m is set
{0} is functional non empty V12() V39(1) V62() V63() V64() V65() V66() V67() set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
rng <*0*> is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() Element of K19(REAL)
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
m . 1 is V43() real integer ext-real set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
<*1*> is Relation-like NAT -defined NAT -valued INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V56() decreasing non-decreasing non-increasing FinSequence of NAT
[1,1] is set
{[1,1]} is Relation-like Function-like constant non empty V12() V39(1) set
m is set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
rng <*1*> is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() Element of K19(REAL)
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
z is V43() real ext-real set
rng m is V62() V63() V64() V65() V66() Element of K19(REAL)
u is Relation-like non non-empty NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product u is V43() real integer ext-real set
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . m is V43() real integer ext-real set
<*1*> is Relation-like NAT -defined NAT -valued INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V56() decreasing non-decreasing non-increasing FinSequence of NAT
[1,1] is set
{[1,1]} is Relation-like Function-like constant non empty V12() V39(1) set
m is set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
rng <*1*> is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() Element of K19(REAL)
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m . z is V43() real integer ext-real set
m . c is V43() real integer ext-real set
z is V43() real ext-real set
rng m is V62() V63() V64() V65() V66() Element of K19(REAL)
u is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
dom u is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
u . m is V43() real integer ext-real set
rng u is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u | m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg m is V32() V39(m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
u | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
len z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len u) is non empty V32() V39( len u) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len u ) } is set
dom u is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . s is V43() real integer ext-real set
z . s is V43() real integer ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . i is V43() real integer ext-real set
z . i is V43() real integer ext-real set
z . c is V43() real integer ext-real set
z . i is V43() real integer ext-real set
c is V43() real ext-real set
rng z is V62() V63() V64() V65() V66() Element of K19(REAL)
i is set
z . i is V43() real integer ext-real set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . s is V43() real integer ext-real set
rng u is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product u is V43() real integer ext-real set
len u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
z | m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg m is V32() V39(m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
z | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
z . (m + 1) is V43() real integer ext-real set
<*(z . (m + 1))*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(z . (m + 1))] is set
{[1,(z . (m + 1))]} is Relation-like Function-like constant non empty V12() V39(1) set
i ^ <*(z . (m + 1))*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg (m + 1) is non empty V32() V39(m + 1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= m + 1 ) } is set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
len i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product i is V43() real integer ext-real set
(Product i) * (z . (m + 1)) is V43() real integer ext-real set
0 * (z . (m + 1)) is V43() real integer ext-real set
Product z is V43() real integer ext-real set
z . 1 is V43() real integer ext-real set
<*(z . 1)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(z . 1)] is set
{[1,(z . 1)]} is Relation-like Function-like constant non empty V12() V39(1) set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
Product z is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product z is V43() real integer ext-real set
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product m is V43() real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product u is V43() real integer ext-real set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom u is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . m is V43() real integer ext-real set
(Product u) / (u . m) is V43() real ext-real set
(u . m) " is V43() real ext-real set
(Product u) * ((u . m) ") is V43() real ext-real set
z is V43() real integer ext-real set
len u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
i | c is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg c is V32() V39(c) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= c ) } is set
i | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
c + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
i . (c + 1) is V43() real integer ext-real set
<*(i . (c + 1))*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(i . (c + 1))] is set
{[1,(i . (c + 1))]} is Relation-like Function-like constant non empty V12() V39(1) set
(i | c) ^ <*(i . (c + 1))*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i | (c + 1) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg (c + 1) is non empty V32() V39(c + 1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= c + 1 ) } is set
i | (Seg (c + 1)) is Relation-like NAT -defined Seg (c + 1) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len (i | c) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom i is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
v is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
cc is V43() real integer ext-real set
Product i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
i . i is V43() real integer ext-real set
(Product i) / (i . i) is V43() real ext-real set
(i . i) " is V43() real ext-real set
(Product i) * ((i . i) ") is V43() real ext-real set
a is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom a is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i . v is V43() real integer ext-real set
Product a is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
a . v is V43() real integer ext-real set
(Product a) / (a . v) is V43() real ext-real set
(a . v) " is V43() real ext-real set
(Product a) * ((a . v) ") is V43() real ext-real set
b is V43() real integer ext-real set
b * (i . (c + 1)) is V43() real integer ext-real set
(i . v) gcd (b * (i . (c + 1))) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(i . v) gcd (i . (c + 1)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(Product a) * (i . (c + 1)) is V43() real integer ext-real set
(i . v) " is V43() real ext-real set
((Product a) * (i . (c + 1))) * ((i . v) ") is V43() real ext-real set
a is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom a is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
rng i is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
len a is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
a | (len a) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg (len a) is non empty V32() V39( len a) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len a ) } is set
a | (Seg (len a)) is Relation-like NAT -defined Seg (len a) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
b is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len i) is non empty V32() V39( len i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len i ) } is set
a . (b + 1) is V43() real integer ext-real set
i . (b + 1) is V43() real integer ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
a | r is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg r is V32() V39(r) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
a | (Seg r) is Relation-like NAT -defined Seg r -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product (a | r) is V43() real integer ext-real set
(Product (a | r)) * (i . (b + 1)) is V43() real integer ext-real set
((Product (a | r)) * (i . (b + 1))) gcd (i . (c + 1)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(i . (b + 1)) gcd (i . (c + 1)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
a . s is V43() real integer ext-real set
<*(a . s)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(a . s)] is set
{[1,(a . s)]} is Relation-like Function-like constant non empty V12() V39(1) set
(a | r) ^ <*(a . s)*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
a | s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg s is V32() V39(s) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= s ) } is set
a | (Seg s) is Relation-like NAT -defined Seg s -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product (a | s) is V43() real integer ext-real set
(Product (a | s)) gcd (i . (c + 1)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
r is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
a | r is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg r is V32() V39(r) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
a | (Seg r) is Relation-like NAT -defined Seg r -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product (a | r) is V43() real integer ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
a | r is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg r is V32() V39(r) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
a | (Seg r) is Relation-like NAT -defined Seg r -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product (a | r) is V43() real integer ext-real set
a | 0 is Relation-like non-empty empty-yielding NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( 0 ) V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
a | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
b is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
a | b is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg b is V32() V39(b) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= b ) } is set
a | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Product (a | b) is V43() real integer ext-real set
Product a is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(Product a) * (i . (c + 1)) is V43() real integer ext-real set
(i . (c + 1)) " is V43() real ext-real set
((Product a) * (i . (c + 1))) * ((i . (c + 1)) ") is V43() real ext-real set
(i . (c + 1)) * ((i . (c + 1)) ") is V43() real ext-real set
(Product a) * ((i . (c + 1)) * ((i . (c + 1)) ")) is V43() real ext-real set
(Product a) * 1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
a is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom a is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i . 1 is V43() real integer ext-real set
<*(i . 1)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(i . 1)] is set
{[1,(i . 1)]} is Relation-like Function-like constant non empty V12() V39(1) set
i is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
dom i is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is V43() real integer ext-real set
Product i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
i . s is V43() real integer ext-real set
(Product i) / (i . s) is V43() real ext-real set
(i . s) " is V43() real ext-real set
(Product i) * ((i . s) ") is V43() real ext-real set
c is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len c is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
dom c is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
s is V43() real integer ext-real set
Product c is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
c . i is V43() real integer ext-real set
(Product c) / (c . i) is V43() real ext-real set
(c . i) " is V43() real ext-real set
(Product c) * ((c . i) ") is V43() real ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
dom m is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is V43() real integer ext-real set
c is V43() real integer ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u . i is V43() real integer ext-real set
m . i is V43() real integer ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
m | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
m | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len m) is non empty V32() V39( len m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len m ) } is set
i is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
m | (i + 1) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg (i + 1) is non empty V32() V39(i + 1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i + 1 ) } is set
m | (Seg (i + 1)) is Relation-like NAT -defined Seg (i + 1) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len i) is non empty V32() V39( len i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len i ) } is set
dom i is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Product i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
i . (i + 1) is V43() real integer ext-real set
(Product i) / (i . (i + 1)) is V43() real ext-real set
(i . (i + 1)) " is V43() real ext-real set
(Product i) * ((i . (i + 1)) ") is V43() real ext-real set
v is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product v is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
m . (i + 1) is V43() real integer ext-real set
rng m is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
b is V43() real integer ext-real set
b * (i . (i + 1)) is V43() real integer ext-real set
((i . (i + 1)) ") * (i . (i + 1)) is V43() real ext-real set
(Product i) * (((i . (i + 1)) ") * (i . (i + 1))) is V43() real ext-real set
(Product i) * 1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
a is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
a | (i + 1) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
a | (Seg (i + 1)) is Relation-like NAT -defined Seg (i + 1) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(a | (i + 1)) | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
(a | (i + 1)) | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
a | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
a | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
<*(i . (i + 1))*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(i . (i + 1))] is set
{[1,(i . (i + 1))]} is Relation-like Function-like constant non empty V12() V39(1) set
v ^ <*(i . (i + 1))*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Product v) * (i . (i + 1)) is V43() real integer ext-real set
(i . (i + 1)) * ((i . (i + 1)) ") is V43() real ext-real set
(Product v) * ((i . (i + 1)) * ((i . (i + 1)) ")) is V43() real ext-real set
(Product v) * 1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
i . 1 is V43() real integer ext-real set
<*(i . 1)*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,(i . 1)] is set
{[1,(i . 1)]} is Relation-like Function-like constant non empty V12() V39(1) set
Product i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
m . 1 is V43() real integer ext-real set
s is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product s is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
m | (len m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m | (Seg (len m)) is Relation-like NAT -defined Seg (len m) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m | 0 is Relation-like non-empty empty-yielding NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( 0 ) V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
m | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
i is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product i is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
z mod (Product m) is V43() real integer ext-real set
c mod (Product m) is V43() real integer ext-real set
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is V43() real integer ext-real set
Seg (len m) is V32() V39( len m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len m ) } is set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m . z is V43() real integer ext-real set
u mod (m . z) is V43() real integer ext-real set
c is V43() real integer V47() ext-real Element of INT
z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
len z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z . c is V43() real integer ext-real set
m . c is V43() real integer ext-real set
u mod (m . c) is V43() real integer ext-real set
z is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
c is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
len c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom c is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len z) is V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
i is set
z . i is set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m . s is V43() real integer ext-real set
u mod (m . s) is V43() real integer ext-real set
c . i is set
u is V43() real integer ext-real set
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,m) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
z is set
rng (u,m) is set
dom (u,m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
c is set
(u,m) . c is set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m . s is V43() real integer ext-real set
u mod (m . s) is V43() real integer ext-real set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
Seg (len u) is non empty V32() V39( len u) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len u ) } is set
m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . m is V43() real integer ext-real set
(Product u) / (u . m) is V43() real ext-real set
(u . m) " is V43() real ext-real set
(Product u) * ((u . m) ") is V43() real ext-real set
dom u is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is V43() real integer ext-real set
c is V43() real integer ext-real set
c * z is V43() real integer ext-real set
s is V43() real integer V47() ext-real Element of INT
c * ((Product u) / (u . m)) is V43() real ext-real set
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . z is V43() real integer ext-real set
(Product u) / (u . z) is V43() real ext-real set
(u . z) " is V43() real ext-real set
(Product u) * ((u . z) ") is V43() real ext-real set
m . z is V43() real integer ext-real set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
m is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like (u)
z is set
rng m is set
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
c is set
m . c is set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
s is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . s is V43() real integer ext-real set
(Product u) / (u . s) is V43() real ext-real set
(u . s) " is V43() real ext-real set
(Product u) * ((u . s) ") is V43() real ext-real set
m . s is set
v is V43() real integer ext-real set
i is V43() real integer ext-real set
i * v is V43() real integer ext-real set
i * ((Product u) / (u . s)) is V43() real ext-real set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (u)
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m . z is V43() real integer ext-real set
u . z is V43() real integer ext-real set
Product u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(Product u) / (u . z) is V43() real ext-real set
(u . z) " is V43() real ext-real set
(Product u) * ((u . z) ") is V43() real ext-real set
i is V43() real integer ext-real set
c is V43() real integer ext-real set
c * i is V43() real integer ext-real set
c * ((Product u) / (u . z)) is V43() real ext-real set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (u)
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m . z is V43() real integer ext-real set
u . c is V43() real integer ext-real set
Product u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
u . z is V43() real integer ext-real set
(Product u) / (u . z) is V43() real ext-real set
(u . z) " is V43() real ext-real set
(Product u) * ((u . z) ") is V43() real ext-real set
s is V43() real integer ext-real set
i is V43() real integer ext-real set
i * s is V43() real integer ext-real set
i * ((Product u) / (u . z)) is V43() real ext-real set
len u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom u is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len m) is V32() V39( len m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len m ) } is set
i is V43() real integer ext-real set
i * (u . c) is V43() real integer ext-real set
i * 0 is V43() real integer ext-real set
i * 0 is V43() real integer ext-real set
u is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
m is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (u)
dom m is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (u)
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
m . c is V43() real integer ext-real set
z . c is V43() real integer ext-real set
u . c is V43() real integer ext-real set
Product u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(Product u) / (u . c) is V43() real ext-real set
(u . c) " is V43() real ext-real set
(Product u) * ((u . c) ") is V43() real ext-real set
len m is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len u is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len m) is V32() V39( len m) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len m ) } is set
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
s is V43() real integer ext-real set
i is V43() real integer ext-real set
i * s is V43() real integer ext-real set
i * ((Product u) / (u . c)) is V43() real ext-real set
v is V43() real integer ext-real set
i is V43() real integer ext-real set
i * v is V43() real integer ext-real set
i * ((Product u) / (u . c)) is V43() real ext-real set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom m is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
u (#) z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) z) is V43() real integer ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . c is V43() real integer ext-real set
m . c is V43() real integer ext-real set
len z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len z) is V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
dom z is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg i is V32() V39(i) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
u | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
v is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
cc is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
v (#) cc is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u | i) (#) (z | i) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u | (i + 1) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Seg (i + 1) is non empty V32() V39(i + 1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= i + 1 ) } is set
u | (Seg (i + 1)) is Relation-like NAT -defined Seg (i + 1) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z | (i + 1) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z | (Seg (i + 1)) is Relation-like NAT -defined Seg (i + 1) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len v is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len v) is V32() V39( len v) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len v ) } is set
dom v is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
v . (i + 1) is V43() real integer ext-real set
u . (i + 1) is V43() real integer ext-real set
cc . (i + 1) is V43() real integer ext-real set
(v . (i + 1)) * (cc . (i + 1)) is V43() real integer ext-real set
r is V43() real ext-real Element of REAL
<*r*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing FinSequence of REAL
[1,r] is set
{[1,r]} is Relation-like Function-like constant non empty V12() V39(1) set
len cc is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len cc) is V32() V39( len cc) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len cc ) } is set
dom cc is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
z . (i + 1) is V43() real integer ext-real set
(u (#) z) | i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u (#) z) | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
<*((v . (i + 1)) * (cc . (i + 1)))*> is Relation-like NAT -defined INT -valued Function-like one-to-one constant non empty V12() V32() V39(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V56() decreasing non-decreasing non-increasing set
[1,((v . (i + 1)) * (cc . (i + 1)))] is set
{[1,((v . (i + 1)) * (cc . (i + 1)))]} is Relation-like Function-like constant non empty V12() V39(1) set
((u (#) z) | i) ^ <*((v . (i + 1)) * (cc . (i + 1)))*> is Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u (#) z) | (i + 1) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u (#) z) | (Seg (i + 1)) is Relation-like NAT -defined Seg (i + 1) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len (u (#) z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (((u (#) z) | i) ^ <*((v . (i + 1)) * (cc . (i + 1)))*>) is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u (#) z) | i) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
(len ((u (#) z) | i)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u (#) z) | (i + 1)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
dom ((u (#) z) | i) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom ((u (#) z) | (i + 1)) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(((u (#) z) | i) ^ <*((v . (i + 1)) * (cc . (i + 1)))*>) . j is V43() real integer ext-real set
((u (#) z) | i) . j is V43() real integer ext-real set
(u (#) z) . j is V43() real integer ext-real set
((u (#) z) | (i + 1)) . j is V43() real integer ext-real set
dom ((u (#) z) | i) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom <*((v . (i + 1)) * (cc . (i + 1)))*> is non empty V12() V39(1) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(((u (#) z) | i) ^ <*((v . (i + 1)) * (cc . (i + 1)))*>) . (i + 1) is V43() real integer ext-real set
<*((v . (i + 1)) * (cc . (i + 1)))*> . 1 is V43() real integer ext-real set
Seg (len (u (#) z)) is V32() V39( len (u (#) z)) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len (u (#) z) ) } is set
dom (u (#) z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom ((u (#) z) | (i + 1)) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
((u (#) z) | (i + 1)) . j is V43() real integer ext-real set
(u (#) z) . j is V43() real integer ext-real set
(((u (#) z) | i) ^ <*((v . (i + 1)) * (cc . (i + 1)))*>) . j is V43() real integer ext-real set
dom ((u (#) z) | i) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
a is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
b is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
s is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
b ^ s is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (v (#) cc) is V43() real integer ext-real set
Sum b is V43() real ext-real Element of REAL
Sum s is V43() real ext-real Element of REAL
(Sum b) + (Sum s) is V43() real ext-real set
Sum ((u | i) (#) (z | i)) is V43() real integer ext-real set
(Sum ((u | i) (#) (z | i))) + ((v . (i + 1)) * (cc . (i + 1))) is V43() real integer ext-real set
(v . (i + 1)) * 0 is V43() real integer ext-real set
0 + ((v . (i + 1)) * 0) is V43() real integer ext-real set
(u . (i + 1)) * 1 is V43() real integer ext-real set
0 + (u . c) is V43() real integer ext-real set
(u . (i + 1)) * 0 is V43() real integer ext-real set
(u . c) + 0 is V43() real integer ext-real set
0 + (u . c) is V43() real integer ext-real set
(u . c) + 0 is V43() real integer ext-real set
0 + (u . c) is V43() real integer ext-real set
(u . c) + 0 is V43() real integer ext-real set
s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
s (#) i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (s (#) i) is V43() real integer ext-real set
Seg (len u) is V32() V39( len u) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len u ) } is set
i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u | 0 is Relation-like non-empty empty-yielding NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( 0 ) V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
u | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z | 0 is Relation-like non-empty empty-yielding NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
z | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V43() real integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V62() V63() V64() V65() V66() V67() V68() set
dom i is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
dom s is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(dom i) /\ (dom s) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i (#) s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (i (#) s) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Sum (i (#) s) is V43() real integer ext-real set
i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i (#) s is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (i (#) s) is V43() real integer ext-real set
z | (len u) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z | (Seg (len u)) is Relation-like NAT -defined Seg (len u) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u | (len u) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u | (Seg (len u)) is Relation-like NAT -defined Seg (len u) -defined NAT -defined INT -valued Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
u (#) z is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) z) is V43() real integer ext-real set
c is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
u (#) c is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) c) is V43() real integer ext-real set
(Sum (u (#) z)) mod (Product m) is V43() real integer ext-real set
(Sum (u (#) c)) mod (Product m) is V43() real integer ext-real set
dom m is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . i is V43() real integer ext-real set
m . i is V43() real integer ext-real set
((Sum (u (#) z)) mod (Product m)) mod (Product m) is V43() real integer ext-real set
rng m is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
v is V43() real integer ext-real set
v * (m . i) is V43() real integer ext-real set
((Sum (u (#) z)) mod (Product m)) mod (m . i) is V43() real integer ext-real set
(Sum (u (#) z)) mod (m . i) is V43() real integer ext-real set
(u . i) mod (m . i) is V43() real integer ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . i is V43() real integer ext-real set
m . i is V43() real integer ext-real set
((Sum (u (#) c)) mod (Product m)) mod (Product m) is V43() real integer ext-real set
rng m is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
v is V43() real integer ext-real set
v * (m . i) is V43() real integer ext-real set
((Sum (u (#) c)) mod (Product m)) mod (m . i) is V43() real integer ext-real set
(Sum (u (#) c)) mod (m . i) is V43() real integer ext-real set
(u . i) mod (m . i) is V43() real integer ext-real set
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)) is V43() real integer ext-real set
(Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m))) mod (Product m) is V43() real integer ext-real set
i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
u (#) i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) i) is V43() real integer ext-real set
(Sum (u (#) i)) mod (Product m) is V43() real integer ext-real set
i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
u (#) i is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) i) is V43() real integer ext-real set
(Sum (u (#) i)) mod (Product m) is V43() real integer ext-real set
the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
c is V43() real integer ext-real set
i is V43() real integer ext-real set
u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)) is V43() real integer ext-real set
(Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m))) mod (Product m) is V43() real integer ext-real set
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
(u,m) is V43() real integer ext-real set
Product m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)) is V43() real integer ext-real set
(Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m))) mod (Product m) is V43() real integer ext-real set
u is V43() real integer ext-real set
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom m is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
z is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
(u,m) . z is V43() real integer ext-real set
m . z is V43() real integer ext-real set
len (u,m) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
rng m is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
u mod (m . z) is V43() real integer ext-real set
u div (m . z) is V43() real integer ext-real set
(u div (m . z)) * (m . z) is V43() real integer ext-real set
u - ((u div (m . z)) * (m . z)) is V43() real integer ext-real set
- ((u div (m . z)) * (m . z)) is V43() real integer ext-real set
u + (- ((u div (m . z)) * (m . z))) is V43() real integer ext-real set
u - (u mod (m . z)) is V43() real integer ext-real set
- (u mod (m . z)) is V43() real integer ext-real set
u + (- (u mod (m . z))) is V43() real integer ext-real set
dom (u,m) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len (u,m)) is V32() V39( len (u,m)) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len (u,m) ) } is set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u + m is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) + (m,z) is Relation-like NAT -defined REAL -valued INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u,z) + (m,z)) . c is V43() real integer ext-real set
z . c is V43() real integer ext-real set
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom (m,z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len z) is non empty V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
(m,z) . c is V43() real integer ext-real set
m mod (z . c) is V43() real integer ext-real set
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) + (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom ((u,z) + (m,z)) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) . c is V43() real integer ext-real set
((u,z) . c) + ((m,z) . c) is V43() real integer ext-real set
dom (u,z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
u mod (z . c) is V43() real integer ext-real set
(((u,z) . c) + ((m,z) . c)) mod (z . c) is V43() real integer ext-real set
(u + m) mod (z . c) is V43() real integer ext-real set
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u - m is V43() real integer ext-real set
- m is V43() real integer ext-real set
u + (- m) is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) - (m,z) is Relation-like NAT -defined REAL -valued INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u,z) - (m,z)) . c is V43() real integer ext-real set
z . c is V43() real integer ext-real set
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom (m,z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len z) is non empty V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
(m,z) . c is V43() real integer ext-real set
m mod (z . c) is V43() real integer ext-real set
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) - (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom ((u,z) - (m,z)) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) . c is V43() real integer ext-real set
((u,z) . c) - ((m,z) . c) is V43() real integer ext-real set
- ((m,z) . c) is V43() real integer ext-real set
((u,z) . c) + (- ((m,z) . c)) is V43() real integer ext-real set
dom (u,z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
u mod (z . c) is V43() real integer ext-real set
(((u,z) . c) - ((m,z) . c)) mod (z . c) is V43() real integer ext-real set
(u - m) mod (z . c) is V43() real integer ext-real set
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u * m is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) (#) (m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u,z) (#) (m,z)) . c is V43() real integer ext-real set
z . c is V43() real integer ext-real set
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom (m,z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len z) is non empty V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
(m,z) . c is V43() real integer ext-real set
m mod (z . c) is V43() real integer ext-real set
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) (#) (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom ((u,z) (#) (m,z)) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) . c is V43() real integer ext-real set
((u,z) . c) * ((m,z) . c) is V43() real integer ext-real set
dom (u,z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
u mod (z . c) is V43() real integer ext-real set
(((u,z) . c) * ((m,z) . c)) mod (z . c) is V43() real integer ext-real set
(u * m) mod (z . c) is V43() real integer ext-real set
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u + m is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) + (m,z) is Relation-like NAT -defined REAL -valued INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(((u,z) + (m,z)),z) is V43() real integer ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z . c is V43() real integer ext-real set
the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z)
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) + (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
((u,z) + (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (((u,z) + (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z)) is V43() real integer ext-real set
Product z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(Sum (((u,z) + (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z))) mod (Product z) is V43() real integer ext-real set
(((u,z) + (m,z)),z) mod (Product z) is V43() real integer ext-real set
i is V43() real integer ext-real set
i * (z . c) is V43() real integer ext-real set
((u,z) + (m,z)) . c is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u - m is V43() real integer ext-real set
- m is V43() real integer ext-real set
u + (- m) is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) - (m,z) is Relation-like NAT -defined REAL -valued INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(((u,z) - (m,z)),z) is V43() real integer ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z . c is V43() real integer ext-real set
the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z)
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) - (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
((u,z) - (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (((u,z) - (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z)) is V43() real integer ext-real set
Product z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(Sum (((u,z) - (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z))) mod (Product z) is V43() real integer ext-real set
(((u,z) - (m,z)),z) mod (Product z) is V43() real integer ext-real set
i is V43() real integer ext-real set
i * (z . c) is V43() real integer ext-real set
((u,z) - (m,z)) . c is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u * m is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) (#) (m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(((u,z) (#) (m,z)),z) is V43() real integer ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
z . c is V43() real integer ext-real set
the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z)
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) (#) (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
((u,z) (#) (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (((u,z) (#) (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z)) is V43() real integer ext-real set
Product z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(Sum (((u,z) (#) (m,z)) (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (z))) mod (Product z) is V43() real integer ext-real set
(((u,z) (#) (m,z)),z) mod (Product z) is V43() real integer ext-real set
i is V43() real integer ext-real set
i * (z . c) is V43() real integer ext-real set
((u,z) (#) (m,z)) . c is V43() real integer ext-real set
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u + m is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) + (m,z) is Relation-like NAT -defined REAL -valued INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(((u,z) + (m,z)),z) is V43() real integer ext-real set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
((u + m),z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u + m),z) . i is V43() real integer ext-real set
z . i is V43() real integer ext-real set
len ((u + m),z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u + m),z) . i is V43() real integer ext-real set
z . i is V43() real integer ext-real set
(((u,z) + (m,z)),z) mod (z . i) is V43() real integer ext-real set
(u + m) mod (z . i) is V43() real integer ext-real set
dom ((u + m),z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len z) is non empty V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
((u + m) mod (z . i)) mod (z . i) is V43() real integer ext-real set
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) + (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u - m is V43() real integer ext-real set
- m is V43() real integer ext-real set
u + (- m) is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) - (m,z) is Relation-like NAT -defined REAL -valued INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(((u,z) - (m,z)),z) is V43() real integer ext-real set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
((u - m),z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u - m),z) . i is V43() real integer ext-real set
z . i is V43() real integer ext-real set
len ((u - m),z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u - m),z) . i is V43() real integer ext-real set
z . i is V43() real integer ext-real set
(((u,z) - (m,z)),z) mod (z . i) is V43() real integer ext-real set
(u - m) mod (z . i) is V43() real integer ext-real set
dom ((u - m),z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len z) is non empty V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
((u - m) mod (z . i)) mod (z . i) is V43() real integer ext-real set
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) - (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is V43() real integer ext-real set
m is V43() real integer ext-real set
u * m is V43() real integer ext-real set
z is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(u,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(u,z) (#) (m,z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(((u,z) (#) (m,z)),z) is V43() real integer ext-real set
dom z is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
((u * m),z) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u * m),z) . i is V43() real integer ext-real set
z . i is V43() real integer ext-real set
len ((u * m),z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len z is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
((u * m),z) . i is V43() real integer ext-real set
z . i is V43() real integer ext-real set
(((u,z) (#) (m,z)),z) mod (z . i) is V43() real integer ext-real set
(u * m) mod (z . i) is V43() real integer ext-real set
dom ((u * m),z) is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len z) is non empty V32() V39( len z) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len z ) } is set
rng z is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
((u * m) mod (z . i)) mod (z . i) is V43() real integer ext-real set
len (u,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len (m,z) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
len ((u,z) (#) (m,z)) is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len u is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT
dom u is V62() V63() V64() V65() V66() V67() Element of K19(NAT)
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
len m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real positive non negative V62() V63() V64() V65() V66() V67() Element of NAT
Product m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
(u,m) is V43() real integer ext-real set
z is V43() real integer ext-real set
the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)
i is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m) is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m)) is V43() real integer ext-real set
(Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m))) mod (Product m) is V43() real integer ext-real set
((Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m))) mod (Product m)) mod (Product m) is V43() real integer ext-real set
dom m is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
Seg (len u) is V32() V39( len u) V62() V63() V64() V65() V66() V67() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer V47() ext-real non negative V62() V63() V64() V65() V66() V67() Element of NAT : ( 1 <= b1 & b1 <= len u ) } is set
m . i is V43() real integer ext-real set
i is V43() real integer ext-real set
i * (m . i) is V43() real integer ext-real set
((Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m))) mod (Product m)) mod (m . i) is V43() real integer ext-real set
(Sum (u (#) the Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued (m))) mod (m . i) is V43() real integer ext-real set
rng m is non empty V62() V63() V64() V65() V66() Element of K19(REAL)
u . i is V43() real integer ext-real set
(u . i) mod (m . i) is V43() real integer ext-real set
c is epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real non negative set
u . c is V43() real integer ext-real set
m . c is V43() real integer ext-real set
z is V43() real integer ext-real set
m is Relation-like non-empty NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding () set
Product m is non empty epsilon-transitive epsilon-connected ordinal natural V32() V37() V43() real integer ext-real positive non negative set
dom m is non empty V62() V63() V64() V65() V66() V67() Element of K19(NAT)
u is Relation-like NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
c is V43() real integer ext-real set