REAL is set
NAT is non empty V23() V24() V25() V30() V35() V36() Element of K19(REAL)
K19(REAL) is set
NAT is non empty V23() V24() V25() V30() V35() V36() set
K19(NAT) is V30() set
K19(NAT) is V30() set
COMPLEX is set
{} is functional empty V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-membered V42() V43() V44() ext-real non positive non negative set
1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
{{},1} is non empty set
RAT is set
INT is set
2 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
K20(NAT,REAL) is set
K19(K20(NAT,REAL)) is set
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = 1 } is set
3 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
0 is functional empty V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-membered V42() V43() V44() ext-real non positive non negative Element of NAT
L is non empty set
a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x is Relation-like NAT -defined L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of L
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x | (a -' 1) is Relation-like NAT -defined L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of L
x . a is set
<*(x . a)*> is Relation-like NAT -defined Function-like non empty trivial V30() V37(1) FinSequence-like FinSubsequence-like set
(x | (a -' 1)) ^ <*(x . a)*> is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like set
x /^ a is Relation-like NAT -defined L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of L
((x | (a -' 1)) ^ <*(x . a)*>) ^ (x /^ a) is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like set
L is non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
the carrier of L is non empty set
0. L is V54(L) right_add-cancelable Element of the carrier of L
x is right_add-cancelable Element of the carrier of L
x * (0. L) is right_add-cancelable Element of the carrier of L
(0. L) + (0. L) is right_add-cancelable Element of the carrier of L
x * ((0. L) + (0. L)) is right_add-cancelable Element of the carrier of L
(x * (0. L)) + (x * (0. L)) is right_add-cancelable Element of the carrier of L
(0. L) + (x * (0. L)) is right_add-cancelable Element of the carrier of L
L is non empty right_add-cancelable unital associative commutative right-distributive right_unital well-unital left_unital left_zeroed doubleLoopStr
the carrier of L is non empty set
x is right_add-cancelable Element of the carrier of L
a is right_add-cancelable Element of the carrier of L
x * a is right_add-cancelable Element of the carrier of L
0. L is V54(L) right_add-cancelable Element of the carrier of L
1. L is right_add-cancelable Element of the carrier of L
b is right_add-cancelable Element of the carrier of L
b * x is right_add-cancelable Element of the carrier of L
b * (0. L) is right_add-cancelable Element of the carrier of L
(1. L) * a is right_add-cancelable Element of the carrier of L
the non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left-distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
(0_. L) *' x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((0_. L) *' x) . a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
b is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Sum b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom b is Element of K19(NAT)
p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
b . p is set
p -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(0_. L) . (p -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a + 1) -' p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((a + 1) -' p) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((0_. L) . (p -' 1)) * (x . ((a + 1) -' p)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * (x . ((a + 1) -' p)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0_. L) . a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty ZeroStr
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
len (0_. L) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
(0_. L) . x is Element of the carrier of L
L is non empty non degenerated non trivial multLoopStr_0
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
the carrier of L is non empty non trivial set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
1. L is V54(L) Element of the carrier of L
(0_. L) +* (0,(1. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
len (1_. L) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(1_. L) . 0 is Element of the carrier of L
x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
(1_. L) . x is Element of the carrier of L
L is non empty ZeroStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is set
dom x is set
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . a is set
L is non empty right_zeroed addLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x + a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len (x + a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x + a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len (x + a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
max ((len x),(len a)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
(len x) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(len a) - 1 is V42() V43() V44() ext-real set
(len a) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((len a) -' 1) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(x + a) . ((len a) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . ((len a) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a . ((len a) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len a) -' 1)) + (a . ((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) + (a . ((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(len (x + a)) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(len a) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(len x) - 1 is V42() V43() V44() ext-real set
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((len x) -' 1) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(x + a) . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) + (a . ((len x) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(len (x + a)) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
- x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len (- x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
x . b is set
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(- x) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- (x . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
(- x) . a is set
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(- x) . a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- (x . a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x - a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
- a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
x + (- a) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len (x - a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len (- a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len a) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . ((len a) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * (a . ((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x *' a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len (x *' a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) + (len a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((len x) + (len a)) - 1 is V42() V43() V44() ext-real set
((len x) + (len a)) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
(x *' a) . b is set
b + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(x *' a) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Sum p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom p is Element of K19(NAT)
(b + 1) - (len a) is V42() V43() V44() ext-real set
- ((b + 1) - (len a)) is V42() V43() V44() ext-real set
- (len x) is V42() V43() V44() ext-real non positive set
q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p . q is set
q -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . (q -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(b + 1) -' q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . ((b + 1) -' q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (q -' 1)) * (a . ((b + 1) -' q)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Seg (len p) is V30() V37( len p) Element of K19(NAT)
(b + 1) - q is V42() V43() V44() ext-real set
q - 1 is V42() V43() V44() ext-real set
- (q - 1) is V42() V43() V44() ext-real set
1 - q is V42() V43() V44() ext-real set
(len a) - (b + 1) is V42() V43() V44() ext-real set
(b + 1) + (1 - q) is V42() V43() V44() ext-real set
((b + 1) - q) + 1 is V42() V43() V44() ext-real set
((b + 1) -' q) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
1 - 1 is V42() V43() V44() ext-real set
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
b + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(((len x) + (len a)) -' 1) - 1 is V42() V43() V44() ext-real set
(((len x) + (len a)) - 1) - 1 is V42() V43() V44() ext-real set
(len a) - 1 is V42() V43() V44() ext-real set
1 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
2 - 2 is V42() V43() V44() ext-real set
((len x) + (len a)) - 2 is V42() V43() V44() ext-real set
((len x) + (len a)) -' 2 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((len x) + (len a)) - (1 + 1) is V42() V43() V44() ext-real set
(((len x) + (len a)) -' 2) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(x *' a) . (((len x) + (len a)) -' 2) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Sum p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom p is Element of K19(NAT)
- 1 is V42() V43() V44() ext-real non positive set
(((len x) + (len a)) - 1) + (- 1) is V42() V43() V44() ext-real set
((((len x) + (len a)) - 1) + (- 1)) + 1 is V42() V43() V44() ext-real set
(len x) + ((len a) - 1) is V42() V43() V44() ext-real set
((((len x) + (len a)) -' 2) + 1) -' (len x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((((len x) + (len a)) -' 2) + 1) - (len x) is V42() V43() V44() ext-real set
(len p) - (len x) is V42() V43() V44() ext-real set
(len x) + 0 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p /^ (len x) is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
dom (p /^ (len x)) is Element of K19(NAT)
len (p /^ (len x)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Seg (len (p /^ (len x))) is V30() V37( len (p /^ (len x))) Element of K19(NAT)
q + (len x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(q + (len x)) - 1 is V42() V43() V44() ext-real set
(q + (len x)) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
q - 1 is V42() V43() V44() ext-real set
(len x) + (q - 1) is V42() V43() V44() ext-real set
Seg (len p) is V30() V37( len p) Element of K19(NAT)
(p /^ (len x)) . q is set
p . (q + (len x)) is set
x . ((q + (len x)) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((((len x) + (len a)) -' 2) + 1) -' (q + (len x)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . (((((len x) + (len a)) -' 2) + 1) -' (q + (len x))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((q + (len x)) -' 1)) * (a . (((((len x) + (len a)) -' 2) + 1) -' (q + (len x)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * (a . (((((len x) + (len a)) -' 2) + 1) -' (q + (len x)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum (p /^ (len x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(len x) - 1 is V42() V43() V44() ext-real set
((len x) - 1) + (len a) is V42() V43() V44() ext-real set
((len x) -' 1) + (len a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p | ((len x) -' 1) is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
dom (p | ((len x) -' 1)) is Element of K19(NAT)
q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len p) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((len p) + 1) - 1 is V42() V43() V44() ext-real set
len (p | ((len x) -' 1)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Seg ((len x) -' 1) is V30() V37((len x) -' 1) Element of K19(NAT)
q + (len a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((((len x) + (len a)) -' 2) + 1) - q is V42() V43() V44() ext-real set
((((len x) + (len a)) -' 2) + 1) -' q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(p | ((len x) -' 1)) . q is set
(p | ((len x) -' 1)) /. q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p /. q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . q is set
q -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . (q -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a . (((((len x) + (len a)) -' 2) + 1) -' q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (q -' 1)) * (a . (((((len x) + (len a)) -' 2) + 1) -' q)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (q -' 1)) * (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum (p | ((len x) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . (len x) is set
<*(p . (len x))*> is Relation-like NAT -defined Function-like non empty trivial V30() V37(1) FinSequence-like FinSubsequence-like set
(p | ((len x) -' 1)) ^ <*(p . (len x))*> is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like set
((p | ((len x) -' 1)) ^ <*(p . (len x))*>) ^ (p /^ (len x)) is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like set
p /. (len x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*(p /. (len x))*> is Relation-like NAT -defined the carrier of L -valued Function-like non empty trivial V30() V37(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L
(p | ((len x) -' 1)) ^ <*(p /. (len x))*> is Relation-like NAT -defined the carrier of L -valued Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
((p | ((len x) -' 1)) ^ <*(p /. (len x))*>) ^ (p /^ (len x)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum ((p | ((len x) -' 1)) ^ <*(p /. (len x))*>) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum ((p | ((len x) -' 1)) ^ <*(p /. (len x))*>)) + (Sum (p /^ (len x))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum <*(p /. (len x))*> is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum (p | ((len x) -' 1))) + (Sum <*(p /. (len x))*>) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((Sum (p | ((len x) -' 1))) + (Sum <*(p /. (len x))*>)) + (Sum (p /^ (len x))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum <*(p /. (len x))*>) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty ZeroStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((len x) -' 1) is Element of the carrier of L
0. L is V54(L) Element of the carrier of L
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(0_. L) +* (((len x) -' 1),(x . ((len x) -' 1))) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
a . ((len x) -' 1) is Element of the carrier of L
dom (0_. L) is set
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . b is Element of the carrier of L
(0_. L) . b is Element of the carrier of L
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
a . ((len x) -' 1) is Element of the carrier of L
b is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
b . ((len x) -' 1) is Element of the carrier of L
p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . p is Element of the carrier of L
b . p is Element of the carrier of L
p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . p is Element of the carrier of L
b . p is Element of the carrier of L
p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty ZeroStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((len x) -' 1) is Element of the carrier of L
(0_. L) +* (((len x) -' 1),(x . ((len x) -' 1))) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
a . b is Element of the carrier of L
(0_. L) . b is Element of the carrier of L
dom (0_. L) is set
a . ((len x) -' 1) is Element of the carrier of L
L is non empty ZeroStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0. L is V54(L) Element of the carrier of L
a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
(L,x) . a is set
a + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(a + 1) - 1 is V42() V43() V44() ext-real set
(len x) - 1 is V42() V43() V44() ext-real set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((len x) -' 1) is Element of the carrier of L
(0_. L) +* (((len x) -' 1),(x . ((len x) -' 1))) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(0 + 1) - 1 is V42() V43() V44() ext-real set
(L,x) . a is Element of the carrier of L
(0_. L) . a is Element of the carrier of L
dom (0_. L) is set
(L,x) . a is Element of the carrier of L
(0_. L) . a is Element of the carrier of L
(L,x) . a is Element of the carrier of L
x . 0 is Element of the carrier of L
(0_. L) . 0 is Element of the carrier of L
(L,x) . a is Element of the carrier of L
(L,x) . a is Element of the carrier of L
L is non empty ZeroStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(0_. L) . ((len x) -' 1) is Element of the carrier of L
x . ((len x) -' 1) is Element of the carrier of L
a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(0_. L) . a is Element of the carrier of L
L is non empty ZeroStr
the carrier of L is non empty set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(L,(0_. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len (0_. L) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty non degenerated non trivial multLoopStr_0
the carrier of L is non empty non trivial set
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
1. L is V54(L) Element of the carrier of L
(0_. L) +* (0,(1. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
(L,(1_. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len (1_. L) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len (1_. L)) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
1 -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(1_. L) . x is Element of the carrier of L
(1_. L) . ((len (1_. L)) -' 1) is Element of the carrier of L
L is non empty ZeroStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len (L,x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((len x) -' 1) is Element of the carrier of L
(0_. L) +* (((len x) -' 1),(x . ((len x) -' 1))) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
dom (0_. L) is set
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
b + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(b + 1) - 1 is V42() V43() V44() ext-real set
(len x) - 1 is V42() V43() V44() ext-real set
(L,x) . ((len x) -' 1) is Element of the carrier of L
((len x) -' 1) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
(L,x) . b is set
b + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(b + 1) - 1 is V42() V43() V44() ext-real set
(L,x) . b is Element of the carrier of L
(0_. L) . b is Element of the carrier of L
len (0_. L) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(len x) - 1 is V42() V43() V44() ext-real set
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
a + (L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
((len x) -' 1) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
b + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(b + 1) - 1 is V42() V43() V44() ext-real set
(a + (L,x)) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . b) + ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . b) + ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . b) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a + (L,x)) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . b) + ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) + ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len (L,x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len (a + (L,x)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
max ((len a),(len (L,x))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty unital doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
a is Element of the carrier of L
b is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom b is Element of K19(NAT)
Sum b is Element of the carrier of L
p is Element of the carrier of L
q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
b . q is set
q -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . (q -' 1) is Element of the carrier of L
(power L) . (a,(q -' 1)) is Element of the carrier of L
(x . (q -' 1)) * ((power L) . (a,(q -' 1))) is Element of the carrier of L
b is Element of the carrier of L
p is Element of the carrier of L
q is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum q is Element of the carrier of L
len q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom q is Element of K19(NAT)
LMp is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum LMp is Element of the carrier of L
len LMp is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom LMp is Element of K19(NAT)
Seg (len x) is V30() V37( len x) Element of K19(NAT)
r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
q . r is set
r -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . (r -' 1) is Element of the carrier of L
(power L) . (a,(r -' 1)) is Element of the carrier of L
(x . (r -' 1)) * ((power L) . (a,(r -' 1))) is Element of the carrier of L
LMp . r is set
L is non empty unital doubleLoopStr
the carrier of L is non empty set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0. L is V54(L) Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
x is Element of the carrier of L
(L,(0_. L),x) is Element of the carrier of L
len (0_. L) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
a is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum a is Element of the carrier of L
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom a is Element of K19(NAT)
<*> the carrier of L is Relation-like NAT -defined the carrier of L -valued Function-like functional empty V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() V44() ext-real non positive non negative FinSequence of the carrier of L
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital associative right_unital well-unital left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty non trivial set
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
1. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0_. L) +* (0,(1. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(1_. L),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len (1_. L) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
a is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom a is Element of K19(NAT)
Seg (len a) is V30() V37( len a) Element of K19(NAT)
a . 1 is set
1 -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(1_. L) . (1 -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (x,(1 -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((1_. L) . (1 -' 1)) * ((power L) . (x,(1 -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(1_. L) . 0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((1_. L) . 0) * ((power L) . (x,(1 -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(1. L) * ((power L) . (x,(1 -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (x,0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
1_ L is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*(1. L)*> is Relation-like NAT -defined the carrier of L -valued Function-like non empty trivial V30() V37(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left-distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((0. L) * x) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((0. L) + (0. L)) * x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(((0. L) + (0. L)) * x) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((0. L) * x) + ((0. L) * x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital left-distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
x + a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(x + a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) + (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
max ((len x),(len a)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p - (len x) is V42() V43() V44() ext-real set
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
q is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom q is Element of K19(NAT)
p -' (len q) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p -' (len q)) |-> (0. L) is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p -' (len q)) FinSequence-like FinSubsequence-like Element of (p -' (len q)) -tuples_on the carrier of L
(p -' (len q)) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b1 where b1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of L * : len b1 = p -' (len q) } is set
Seg (p -' (len q)) is V30() V37(p -' (len q)) Element of K19(NAT)
K90((Seg (p -' (len q))),(0. L)) is Relation-like Seg (p -' (len q)) -defined {(0. L)} -valued Function-like total V18( Seg (p -' (len q)),{(0. L)}) V30() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (p -' (len q))),{(0. L)}))
{(0. L)} is non empty trivial V37(1) set
K20((Seg (p -' (len q))),{(0. L)}) is set
K19(K20((Seg (p -' (len q))),{(0. L)})) is set
q ^ ((p -' (len q)) |-> (0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len (q ^ ((p -' (len q)) |-> (0. L))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p -' (len x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(p -' (len x)) |-> (0. L) is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p -' (len x)) FinSequence-like FinSubsequence-like Element of (p -' (len x)) -tuples_on the carrier of L
(p -' (len x)) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b1 where b1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of L * : len b1 = p -' (len x) } is set
Seg (p -' (len x)) is V30() V37(p -' (len x)) Element of K19(NAT)
K90((Seg (p -' (len x))),(0. L)) is Relation-like Seg (p -' (len x)) -defined {(0. L)} -valued Function-like total V18( Seg (p -' (len x)),{(0. L)}) V30() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (p -' (len x))),{(0. L)}))
K20((Seg (p -' (len x))),{(0. L)}) is set
K19(K20((Seg (p -' (len x))),{(0. L)})) is set
len ((p -' (len x)) |-> (0. L)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) + (len ((p -' (len x)) |-> (0. L))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) + (p -' (len x)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) + (p - (len x)) is V42() V43() V44() ext-real set
p - (len a) is V42() V43() V44() ext-real set
len (x + a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p - (len (x + a)) is V42() V43() V44() ext-real set
LMp is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum LMp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len LMp is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom LMp is Element of K19(NAT)
p -' (len LMp) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(p -' (len LMp)) |-> (0. L) is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p -' (len LMp)) FinSequence-like FinSubsequence-like Element of (p -' (len LMp)) -tuples_on the carrier of L
(p -' (len LMp)) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b1 where b1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of L * : len b1 = p -' (len LMp) } is set
Seg (p -' (len LMp)) is V30() V37(p -' (len LMp)) Element of K19(NAT)
K90((Seg (p -' (len LMp))),(0. L)) is Relation-like Seg (p -' (len LMp)) -defined {(0. L)} -valued Function-like total V18( Seg (p -' (len LMp)),{(0. L)}) V30() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (p -' (len LMp))),{(0. L)}))
K20((Seg (p -' (len LMp))),{(0. L)}) is set
K19(K20((Seg (p -' (len LMp))),{(0. L)})) is set
LMp ^ ((p -' (len LMp)) |-> (0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len (LMp ^ ((p -' (len LMp)) |-> (0. L))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p -' (len (x + a)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(p -' (len (x + a))) |-> (0. L) is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p -' (len (x + a))) FinSequence-like FinSubsequence-like Element of (p -' (len (x + a))) -tuples_on the carrier of L
(p -' (len (x + a))) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b1 where b1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of L * : len b1 = p -' (len (x + a)) } is set
Seg (p -' (len (x + a))) is V30() V37(p -' (len (x + a))) Element of K19(NAT)
K90((Seg (p -' (len (x + a)))),(0. L)) is Relation-like Seg (p -' (len (x + a))) -defined {(0. L)} -valued Function-like total V18( Seg (p -' (len (x + a))),{(0. L)}) V30() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (p -' (len (x + a)))),{(0. L)}))
K20((Seg (p -' (len (x + a)))),{(0. L)}) is set
K19(K20((Seg (p -' (len (x + a)))),{(0. L)})) is set
len ((p -' (len (x + a))) |-> (0. L)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len (x + a)) + (len ((p -' (len (x + a))) |-> (0. L))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len (x + a)) + (p -' (len (x + a))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len (x + a)) + (p - (len (x + a))) is V42() V43() V44() ext-real set
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom r is Element of K19(NAT)
p -' (len r) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(p -' (len r)) |-> (0. L) is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p -' (len r)) FinSequence-like FinSubsequence-like Element of (p -' (len r)) -tuples_on the carrier of L
(p -' (len r)) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b1 where b1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of L * : len b1 = p -' (len r) } is set
Seg (p -' (len r)) is V30() V37(p -' (len r)) Element of K19(NAT)
K90((Seg (p -' (len r))),(0. L)) is Relation-like Seg (p -' (len r)) -defined {(0. L)} -valued Function-like total V18( Seg (p -' (len r)),{(0. L)}) V30() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (p -' (len r))),{(0. L)}))
K20((Seg (p -' (len r))),{(0. L)}) is set
K19(K20((Seg (p -' (len r))),{(0. L)})) is set
r ^ ((p -' (len r)) |-> (0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len (r ^ ((p -' (len r)) |-> (0. L))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p -' (len a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(p -' (len a)) |-> (0. L) is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p -' (len a)) FinSequence-like FinSubsequence-like Element of (p -' (len a)) -tuples_on the carrier of L
(p -' (len a)) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b1 where b1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of L * : len b1 = p -' (len a) } is set
Seg (p -' (len a)) is V30() V37(p -' (len a)) Element of K19(NAT)
K90((Seg (p -' (len a))),(0. L)) is Relation-like Seg (p -' (len a)) -defined {(0. L)} -valued Function-like total V18( Seg (p -' (len a)),{(0. L)}) V30() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (p -' (len a))),{(0. L)}))
K20((Seg (p -' (len a))),{(0. L)}) is set
K19(K20((Seg (p -' (len a))),{(0. L)})) is set
len ((p -' (len a)) |-> (0. L)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len a) + (len ((p -' (len a)) |-> (0. L))) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len a) + (p -' (len a)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len a) + (p - (len a)) is V42() V43() V44() ext-real set
p -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b1 where b1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of L * : len b1 = p } is set
k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
Seg p is V30() V37(p) Element of K19(NAT)
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
len j is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom j is V37(p) Element of K19(NAT)
j /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
j . k is set
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom r is V37(p) Element of K19(NAT)
r /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . k is set
q . k is set
q /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (b,(k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Seg (len a) is V30() V37( len a) Element of K19(NAT)
r . k is set
a . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
LMp . k is set
(x + a) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x + a) . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) + (a . (k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) + (a . (k -' 1))) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) * ((power L) . (b,(k -' 1)))) + ((a . (k -' 1)) * ((power L) . (b,(k -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) * ((power L) . (b,(k -' 1)))) + (r /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(q /. k) + (r /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
(len a) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
k - 1 is V42() V43() V44() ext-real set
k - (len r) is V42() V43() V44() ext-real set
p - (len r) is V42() V43() V44() ext-real set
k -' (len r) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((p -' (len r)) |-> (0. L)) . (k - (len r)) is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
LMp . k is set
(x + a) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x + a) . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) + (a . (k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) + (a . (k -' 1))) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) + (0. L)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(r /. k) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom r is V37(p) Element of K19(NAT)
r /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . k is set
j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
len j is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom j is V37(p) Element of K19(NAT)
j /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
j . k is set
r . k is set
r /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (b,(k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Seg (len x) is V30() V37( len x) Element of K19(NAT)
q . k is set
x . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
LMp . k is set
(x + a) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x + a) . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) + (a . (k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) + (a . (k -' 1))) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) * ((power L) . (b,(k -' 1)))) + ((a . (k -' 1)) * ((power L) . (b,(k -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(q /. k) + ((a . (k -' 1)) * ((power L) . (b,(k -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(q /. k) + (r /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
(len x) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
k - 1 is V42() V43() V44() ext-real set
k - (len q) is V42() V43() V44() ext-real set
p - (len q) is V42() V43() V44() ext-real set
k -' (len q) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((p -' (len q)) |-> (0. L)) . (k - (len q)) is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
LMp . k is set
(x + a) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x + a) . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) + (a . (k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) + (a . (k -' 1))) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) + (a . (k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((0. L) + (a . (k -' 1))) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) + (j /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 . k is set
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
len j is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom j is V37(p) Element of K19(NAT)
j /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
j . k is set
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom r is V37(p) Element of K19(NAT)
r /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . k is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
len r1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
q . k is set
k -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (b,(k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . k is set
a . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Seg (len (x + a)) is V30() V37( len (x + a)) Element of K19(NAT)
r1 . k is set
LMp . k is set
(x + a) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x + a) . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) + (a . (k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) + (a . (k -' 1))) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) * ((power L) . (b,(k -' 1)))) + ((a . (k -' 1)) * ((power L) . (b,(k -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) * ((power L) . (b,(k -' 1)))) + (r /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(q /. k) + (r /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
(len (x + a)) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((len (x + a)) + 1) - 1 is V42() V43() V44() ext-real set
k - 1 is V42() V43() V44() ext-real set
k - (len LMp) is V42() V43() V44() ext-real set
p - (len LMp) is V42() V43() V44() ext-real set
r . k is set
a . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k -' (len LMp) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r1 . k is set
((p -' (len LMp)) |-> (0. L)) . (k - (len LMp)) is set
(0. L) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x + a) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x + a) . (k -' 1)) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (k -' 1)) + (a . (k -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) + (a . (k -' 1))) * ((power L) . (b,(k -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . (k -' 1)) * ((power L) . (b,(k -' 1)))) + ((a . (k -' 1)) * ((power L) . (b,(k -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r1 . k is set
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r1 . k is set
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
(r + j) . k is set
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
r + j is Relation-like NAT -defined the carrier of L -valued Function-like V30() V37(p) FinSequence-like FinSubsequence-like Element of p -tuples_on the carrier of L
Sum r1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum ((p -' (len LMp)) |-> (0. L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum LMp) + (Sum ((p -' (len LMp)) |-> (0. L))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum LMp) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum j is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum ((p -' (len r)) |-> (0. L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum r) + (Sum ((p -' (len r)) |-> (0. L))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum r) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum ((p -' (len q)) |-> (0. L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum q) + (Sum ((p -' (len q)) |-> (0. L))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum q) + (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
- x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(- x),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- (L,x,a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
b is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom b is Element of K19(NAT)
len (- x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom p is Element of K19(NAT)
q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
LMp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
b . q is set
p . q is set
q -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(- x) . (q -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (a,(q -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((- x) . (q -' 1)) * ((power L) . (a,(q -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
x . (q -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- (x . (q -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(- (x . (q -' 1))) * ((power L) . (a,(q -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . (q -' 1)) * ((power L) . (a,(q -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- ((x . (q -' 1)) * ((power L) . (a,(q -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- LMp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
x - a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
- a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
x + (- a) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(x - a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) - (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(- a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) + (L,(- a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
- (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) + (- (L,a,b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (a,((len x) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * ((power L) . (a,((len x) -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len (L,x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom p is Element of K19(NAT)
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
Seg (len p) is V30() V37( len p) Element of K19(NAT)
(len x) - 1 is V42() V43() V44() ext-real set
q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
q - 1 is V42() V43() V44() ext-real set
q -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
p /. q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . q is set
(L,x) . (q -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (a,(q -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (q -' 1)) * ((power L) . (a,(q -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * ((power L) . (a,(q -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p /. (len x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . (len x) is set
(L,x) . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . ((len x) -' 1)) * ((power L) . (a,((len x) -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(0. L) * ((power L) . (a,((len x) -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital associative right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,a) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) *' (L,a) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
x . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(len a) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
a . ((len a) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * (a . ((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(len x) + (len a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((len x) + (len a)) -' 2 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(len a) - 1 is V42() V43() V44() ext-real set
(len x) - 1 is V42() V43() V44() ext-real set
1 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
0 + (1 + 1) is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((len x) + (len a)) - 1 is V42() V43() V44() ext-real set
b is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
b -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(b -' 1) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
LMp is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,((L,x) *' (L,a)),LMp) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (LMp,(((len x) + (len a)) -' 2)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . ((len x) -' 1)) * (a . ((len a) -' 1))) * ((power L) . (LMp,(((len x) + (len a)) -' 2))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len ((L,x) *' (L,a)) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Sum r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
dom r is Element of K19(NAT)
((L,x) *' (L,a)) . (b -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Sum r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom r is Element of K19(NAT)
(len x) + 0 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) + ((len a) - 1) is V42() V43() V44() ext-real set
Seg (len r) is V30() V37( len r) Element of K19(NAT)
((len x) + ((len a) - 1)) - (len x) is V42() V43() V44() ext-real set
b -' (len x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r . (len x) is set
(L,x) . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,a) . ((len a) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . ((len x) -' 1)) * ((L,a) . ((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
j is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
j - 1 is V42() V43() V44() ext-real set
j -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r /. j is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . j is set
(L,x) . (j -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((b -' 1) + 1) -' j is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(L,a) . (((b -' 1) + 1) -' j) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (j -' 1)) * ((L,a) . (((b -' 1) + 1) -' j)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * ((L,a) . (((b -' 1) + 1) -' j)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r /. (len x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * ((L,a) . ((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
j is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
j -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(j -' 1) + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((L,x) *' (L,a)) . (j -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len r1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Sum r1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom r1 is Element of K19(NAT)
Seg (len r) is V30() V37( len r) Element of K19(NAT)
k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Seg (len r1) is V30() V37( len r1) Element of K19(NAT)
k - 1 is V42() V43() V44() ext-real set
k -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r1 . k is set
(L,x) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((j -' 1) + 1) -' k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(L,a) . (((j -' 1) + 1) -' k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (k -' 1)) * ((L,a) . (((j -' 1) + 1) -' k)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * ((L,a) . (((j -' 1) + 1) -' k)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0 + k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
j - k is V42() V43() V44() ext-real set
j -' (len x) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
j - (len x) is V42() V43() V44() ext-real set
r1 . k is set
(L,x) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,a) . (j -' (len x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (k -' 1)) * ((L,a) . (j -' (len x))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (k -' 1)) * (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r /. j is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . j is set
(power L) . (LMp,(j -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum r1) * ((power L) . (LMp,(j -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * ((power L) . (LMp,(j -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((len x) + (len a)) - 2 is V42() V43() V44() ext-real set
((len x) + (len a)) - (1 + 1) is V42() V43() V44() ext-real set
(((len x) + (len a)) - 1) - 1 is V42() V43() V44() ext-real set
r /. b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . b is set
j is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
j + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
((L,x) *' (L,a)) . j is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r1 is Relation-like NAT -defined the carrier of L -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
len r1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Sum r1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom r1 is Element of K19(NAT)
k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
k -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r1 . k is set
(L,x) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(j + 1) -' k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(L,a) . ((j + 1) -' k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (k -' 1)) * ((L,a) . ((j + 1) -' k)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * ((L,a) . ((j + 1) -' k)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
Seg (len r1) is V30() V37( len r1) Element of K19(NAT)
k - 1 is V42() V43() V44() ext-real set
0 + k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(j + 1) - k is V42() V43() V44() ext-real set
(j + 1) -' k is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
j - (len x) is V42() V43() V44() ext-real set
(j - (len x)) + 1 is V42() V43() V44() ext-real set
(b -' 1) - (len x) is V42() V43() V44() ext-real set
((b -' 1) - (len x)) + 1 is V42() V43() V44() ext-real set
r1 . k is set
(L,x) . (k -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,a) . ((j + 1) -' k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (k -' 1)) * ((L,a) . ((j + 1) -' k)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . (k -' 1)) * (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
L is non empty non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty non trivial set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,a) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) *' (L,a) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,((L,x) *' (L,a)),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * (L,(L,a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(len a) - 1 is V42() V43() V44() ext-real set
(len a) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(len x) - 1 is V42() V43() V44() ext-real set
(len x) -' 1 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
1 + 1 is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
0 + (1 + 1) is non empty V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real positive non negative Element of NAT
(len x) + (len a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((len x) + (len a)) - 2 is V42() V43() V44() ext-real set
((len x) + (len a)) -' 2 is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
((len x) + (len a)) - (1 + 1) is V42() V43() V44() ext-real set
((len x) - 1) + ((len a) - 1) is V42() V43() V44() ext-real set
x . ((len x) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a . ((len a) -' 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * (a . ((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
power L is Relation-like K20( the carrier of L,NAT) -defined the carrier of L -valued Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))
K20( the carrier of L,NAT) is V30() set
K20(K20( the carrier of L,NAT), the carrier of L) is V30() set
K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V30() set
(power L) . (b,(((len x) + (len a)) -' 2)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . ((len x) -' 1)) * (a . ((len a) -' 1))) * ((power L) . (b,(((len x) + (len a)) -' 2))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (b,((len x) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(power L) . (b,((len a) -' 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((power L) . (b,((len x) -' 1))) * ((power L) . (b,((len a) -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . ((len x) -' 1)) * (a . ((len a) -' 1))) * (((power L) . (b,((len x) -' 1))) * ((power L) . (b,((len a) -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . ((len a) -' 1)) * (((power L) . (b,((len x) -' 1))) * ((power L) . (b,((len a) -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * ((a . ((len a) -' 1)) * (((power L) . (b,((len x) -' 1))) * ((power L) . (b,((len a) -' 1))))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a . ((len a) -' 1)) * ((power L) . (b,((len a) -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((power L) . (b,((len x) -' 1))) * ((a . ((len a) -' 1)) * ((power L) . (b,((len a) -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * (((power L) . (b,((len x) -' 1))) * ((a . ((len a) -' 1)) * ((power L) . (b,((len a) -' 1))))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(x . ((len x) -' 1)) * ((power L) . (b,((len x) -' 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . ((len x) -' 1)) * ((power L) . (b,((len x) -' 1)))) * ((a . ((len a) -' 1)) * ((power L) . (b,((len a) -' 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((x . ((len x) -' 1)) * ((power L) . (b,((len x) -' 1)))) * (L,(L,a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(L,(0_. L),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * (L,(L,a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len (L,a) is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(L,(0_. L),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty non trivial set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) *' a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,((L,x) *' a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
LMp is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len LMp is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
(L,x) *' LMp is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,((L,x) *' LMp),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,LMp,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * (L,LMp,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,LMp) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(len LMp) - 1 is V42() V43() V44() ext-real set
r is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r + (L,LMp) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) *' r is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) *' (L,LMp) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
((L,x) *' r) + ((L,x) *' (L,LMp)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,(((L,x) *' r) + ((L,x) *' (L,LMp))),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,((L,x) *' r),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,((L,x) *' (L,LMp)),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,((L,x) *' r),b) + (L,((L,x) *' (L,LMp)),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,r,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * (L,r,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,(L,x),b) * (L,r,b)) + (L,((L,x) *' (L,LMp)),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,LMp),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * (L,(L,LMp),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,(L,x),b) * (L,r,b)) + ((L,(L,x),b) * (L,(L,LMp),b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,r,b) + (L,(L,LMp),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * ((L,r,b) + (L,(L,LMp),b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(L,(0_. L),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,x),b) * (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len a is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty non trivial set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
x *' a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(x *' a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x,b) * (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative set
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len q is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
q *' a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,(q *' a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,q,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,q,b) * (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,q) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(len q) - 1 is V42() V43() V44() ext-real set
r is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
len r is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
r + (L,q) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
r *' a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,q) *' a is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(r *' a) + ((L,q) *' a) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,((r *' a) + ((L,q) *' a)),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(r *' a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,((L,q) *' a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(r *' a),b) + (L,((L,q) *' a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,r,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,r,b) * (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,r,b) * (L,a,b)) + (L,((L,q) *' a),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,q),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,(L,q),b) * (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,r,b) * (L,a,b)) + ((L,(L,q),b) * (L,a,b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,r,b) + (L,(L,q),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,r,b) + (L,(L,q),b)) * (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
(L,(0_. L),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * (L,a,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len x is V23() V24() V25() V29() V30() V35() V42() V43() V44() ext-real non negative Element of NAT
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
Polynom-Ring L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of (Polynom-Ring L) is non empty set
K20( the carrier of (Polynom-Ring L), the carrier of L) is set
K19(K20( the carrier of (Polynom-Ring L), the carrier of L)) is set
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
b is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,b,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
b is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
b . p is set
(L,p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
b is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
a . p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
b . p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty non trivial set
Polynom-Ring L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
the carrier of (Polynom-Ring L) is non empty set
K20( the carrier of (Polynom-Ring L), the carrier of L) is set
K19(K20( the carrier of (Polynom-Ring L), the carrier of L)) is set
1_ (Polynom-Ring L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
1. (Polynom-Ring L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
(L,x) . (1_ (Polynom-Ring L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
1_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
0_. L is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
0. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K91( the carrier of L,NAT,(0. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) V27() Element of K19(K20(NAT, the carrier of L))
1. L is V54(L) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0_. L) +* (0,(1. L)) is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))
(L,x) . (1_. L) is set
(L,(1_. L),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
1_ L is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty set
Polynom-Ring L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict Abelian add-associative right_zeroed right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
the carrier of (Polynom-Ring L) is non empty set
K20( the carrier of (Polynom-Ring L), the carrier of L) is set
K19(K20( the carrier of (Polynom-Ring L), the carrier of L)) is set
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
a + b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
(L,x) . (a + b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) . a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . a) + ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
a + b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
(L,x) . (a + b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
p + q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) . (p + q) is set
(L,(p + q),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,p,x) + (L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . a) + (L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . a) + ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty non trivial set
Polynom-Ring L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict Abelian add-associative right_zeroed commutative right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) additive Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
the carrier of (Polynom-Ring L) is non empty set
K20( the carrier of (Polynom-Ring L), the carrier of L) is set
K19(K20( the carrier of (Polynom-Ring L), the carrier of L)) is set
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
a * b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
(L,x) . (a * b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) . a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) . b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . a) * ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
K20(NAT, the carrier of L) is V30() set
K19(K20(NAT, the carrier of L)) is V30() set
a * b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring L)
(L,x) . (a * b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
p *' q is Relation-like NAT -defined the carrier of L -valued Function-like non empty total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))
(L,x) . (p *' q) is set
(L,(p *' q),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,p,x) * (L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . a) * (L,q,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((L,x) . a) * ((L,x) . b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
the carrier of L is non empty non trivial set
Polynom-Ring L is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(L,x) is Relation-like the carrier of (Polynom-Ring L) -defined the carrier of L -valued Function-like non empty total V18( the carrier of (Polynom-Ring L), the carrier of L) unity-preserving multiplicative additive Element of K19(K20( the carrier of (Polynom-Ring L), the carrier of L))
the carrier of (Polynom-Ring L) is non empty set
K20( the carrier of (Polynom-Ring L), the carrier of L) is set
K19(K20( the carrier of (Polynom-Ring L), the carrier of L)) is set