:: POLYNOM4 semantic presentation

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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 (