:: TERMORD semantic presentation

REAL is set

NAT is non zero non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K19(REAL)

K19(REAL) is set

NAT is non zero non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

K19(NAT) is non trivial non finite set

K19(NAT) is non trivial non finite set

COMPLEX is set

RAT is set

INT is set

0 is Function-like functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite V34() cardinal 0 -element FinSequence-membered ext-real non positive non negative complex set

2 is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

K20(COMPLEX,COMPLEX) is set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is non trivial non finite set

K20(K20(NAT,NAT),NAT) is non trivial non finite set

K19(K20(K20(NAT,NAT),NAT)) is non trivial non finite set

K20(NAT,REAL) is set

K19(K20(NAT,REAL)) is set

K236() is Relation-like NAT -defined Function-like total set

1 is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

3 is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

0 is Function-like functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite V34() cardinal 0 -element FinSequence-membered ext-real non positive non negative complex Element of NAT

EmptyBag 0 is Relation-like 0 -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags 0

Bags 0 is non zero set

Bags 0 is functional non zero Element of K19((Bags 0))

K19((Bags 0)) is set

the non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V89() V91() V93() right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V89() V91() V93() right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V89() V91() V93() right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible V89() V91() V93() right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

n is set

n is set

O is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is set

O . p is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

L . p is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(O . p) - (O . p) is V28() ext-real complex set

(L . p) - (O . p) is V28() ext-real complex set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

Bags n is non zero set

Bags n is functional non zero Element of K19((Bags n))

K19((Bags n)) is set

O + (EmptyBag n) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is non zero set

{ [b

x9 is set

u9 is Element of p

L . u9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . u9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . u9) -' (O . u9) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

[u9,((L . u9) -' (O . u9))] is V15() set

x9 is set

u9 is set

[x9,u9] is V15() set

k is set

[x9,k] is V15() set

k is Element of p

L . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . k) -' (O . k) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

[k,((L . k) -' (O . k))] is V15() set

b1 is Element of p

L . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . b1) -' (O . b1) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

[b1,((L . b1) -' (O . b1))] is V15() set

u9 is set

x9 is Relation-like Function-like set

dom x9 is set

k is set

[u9,k] is V15() set

k is Element of p

L . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . k) -' (O . k) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

[k,((L . k) -' (O . k))] is V15() set

u9 is set

k is Element of p

L . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . k) -' (O . k) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

[k,((L . k) -' (O . k))] is V15() set

k is set

u9 is Relation-like p -defined Function-like total set

k is set

[k,k] is V15() set

b1 is Element of p

L . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . b1) -' (O . b1) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

[b1,((L . b1) -' (O . b1))] is V15() set

u9 . k is set

L . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . k) -' (O . k) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

support u9 is set

dom u9 is Element of K19(p)

K19(p) is set

k is set

u9 . k is set

support L is finite set

L . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . k) -' (O . k) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

k is set

rng u9 is set

k is set

[k,k] is V15() set

b1 is Element of p

L . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . b1) -' (O . b1) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

[b1,((L . b1) -' (O . b1))] is V15() set

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b1 is set

L . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

O . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(L . b1) - (O . b1) is V28() ext-real complex set

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

k . b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex V156() set

(O . b1) + (k . b1) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex set

(L . b1) -' (O . b1) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

(O . b1) + ((L . b1) -' (O . b1)) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex set

- (O . b1) is V28() ext-real non positive complex set

(L . b1) + (- (O . b1)) is V28() ext-real complex set

(O . b1) + ((L . b1) + (- (O . b1))) is V28() ext-real complex set

O + k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

O + p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

O + x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

O + p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

O + x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

O is non empty left_add-cancelable right_add-cancelable right_complementable V89() right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of O is non zero set

K20((Bags n), the carrier of O) is set

K19(K20((Bags n), the carrier of O)) is set

0_ (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

L is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) Element of K19(K20((Bags n), the carrier of O))

(0_ (n,O)) *' L is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) Element of K19(K20((Bags n), the carrier of O))

x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

((0_ (n,O)) *' L) . x is Element of the carrier of O

decomp x is Relation-like NAT -defined K257(2,(Bags n)) -valued Function-like one-to-one non zero finite FinSequence-like FinSubsequence-like V132() FinSequence-yielding finite-support FinSequence of K257(2,(Bags n))

K257(2,(Bags n)) is M14( Bags n)

len (decomp x) is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

x9 is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of O

Sum x9 is Element of the carrier of O

len x9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

dom x9 is finite Element of K19(NAT)

u9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex set

(decomp x) /. u9 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))

x9 /. u9 is Element of the carrier of O

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*k,k*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

(0_ (n,O)) . k is Element of the carrier of O

L . k is Element of the carrier of O

((0_ (n,O)) . k) * (L . k) is Element of the carrier of O

0. O is zero Element of the carrier of O

(0. O) * (L . k) is Element of the carrier of O

(0_ (n,O)) . x is Element of the carrier of O

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

O is non empty left_add-cancelable right_add-cancelable right_complementable V89() right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of O is non zero set

K20((Bags n), the carrier of O) is set

K19(K20((Bags n), the carrier of O)) is set

L is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

p is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

L *' p is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

Support (L *' p) is functional Element of K19((Bags n))

K19((Bags n)) is set

Support (L *' p) is functional Element of K19((Bags n))

K19((Bags n)) is set

Support L is functional Element of K19((Bags n))

Support p is functional Element of K19((Bags n))

x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

{x} is functional non zero trivial finite 1 -element set

p . x is Element of the carrier of O

0. O is zero Element of the carrier of O

x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p . x9 is Element of the carrier of O

x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

{x9} is functional non zero trivial finite 1 -element set

L . x9 is Element of the carrier of O

u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

L . u9 is Element of the carrier of O

the Relation-like n -defined Function-like Element of Support (L *' p) is Relation-like n -defined Function-like Element of Support (L *' p)

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(L *' p) . k is Element of the carrier of O

decomp k is Relation-like NAT -defined K257(2,(Bags n)) -valued Function-like one-to-one non zero finite FinSequence-like FinSubsequence-like V132() FinSequence-yielding finite-support FinSequence of K257(2,(Bags n))

K257(2,(Bags n)) is M14( Bags n)

len (decomp k) is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

k is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of O

Sum k is Element of the carrier of O

len k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

dom k is finite Element of K19(NAT)

Seg (len (decomp k)) is non zero finite len (decomp k) -element Element of K19(NAT)

dom (decomp k) is finite Element of K19(NAT)

x9 + x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

(decomp k) /. b1 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))

k /. b1 is Element of the carrier of O

b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b2,k*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

L . b2 is Element of the carrier of O

p . k is Element of the carrier of O

(L . b2) * (p . k) is Element of the carrier of O

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b19,b29*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

b19 + b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b19,b29*> . 2 is set

<*b19,b29*> . 1 is set

<*> the carrier of O is Relation-like NAT -defined the carrier of O -valued Function-like one-to-one constant functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite finite-yielding V34() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V132() ext-real non positive non negative complex V170() V171() V172() V173() FinSequence-yielding finite-support M15( the carrier of O,K256( the carrier of O))

K256( the carrier of O) is functional non zero FinSequence-membered M14( the carrier of O)

the Element of dom k is Element of dom k

b2 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

k /. b2 is Element of the carrier of O

k /. the Element of dom k is Element of the carrier of O

b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(L *' p) . b1 is Element of the carrier of O

decomp b1 is Relation-like NAT -defined K257(2,(Bags n)) -valued Function-like one-to-one non zero finite FinSequence-like FinSubsequence-like V132() FinSequence-yielding finite-support FinSequence of K257(2,(Bags n))

len (decomp b1) is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

b2 is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of O

Sum b2 is Element of the carrier of O

len b2 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

dom b2 is finite Element of K19(NAT)

Seg (len (decomp b1)) is non zero finite len (decomp b1) -element Element of K19(NAT)

dom (decomp b1) is finite Element of K19(NAT)

k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

(decomp b1) /. k is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))

b2 /. k is Element of the carrier of O

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b19,b29*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

L . b19 is Element of the carrier of O

p . b29 is Element of the carrier of O

(L . b19) * (p . b29) is Element of the carrier of O

b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b1,b2*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

b1 + b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b1,b2*> . 2 is set

<*b1,b2*> . 1 is set

<*> the carrier of O is Relation-like NAT -defined the carrier of O -valued Function-like one-to-one constant functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite finite-yielding V34() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V132() ext-real non positive non negative complex V170() V171() V172() V173() FinSequence-yielding finite-support M15( the carrier of O,K256( the carrier of O))

K256( the carrier of O) is functional non zero FinSequence-membered M14( the carrier of O)

the Element of dom b2 is Element of dom b2

b19 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

b2 /. b19 is Element of the carrier of O

b2 /. the Element of dom b2 is Element of the carrier of O

Support L is functional Element of K19((Bags n))

Support p is functional Element of K19((Bags n))

0_ (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

0_ (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

Support L is functional Element of K19((Bags n))

Support p is functional Element of K19((Bags n))

Support L is functional Element of K19((Bags n))

Support p is functional Element of K19((Bags n))

Support (L *' p) is functional Element of K19((Bags n))

K19((Bags n)) is set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

O is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of O is non zero set

K20((Bags n), the carrier of O) is set

K19(K20((Bags n), the carrier of O)) is set

L is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

p is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

L *' p is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) Element of K19(K20((Bags n), the carrier of O))

x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

(L *' p) . x9 is Element of the carrier of O

decomp x9 is Relation-like NAT -defined K257(2,(Bags n)) -valued Function-like one-to-one non zero finite FinSequence-like FinSubsequence-like V132() FinSequence-yielding finite-support FinSequence of K257(2,(Bags n))

K257(2,(Bags n)) is M14( Bags n)

len (decomp x9) is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

u9 is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of O

Sum u9 is Element of the carrier of O

len u9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

dom u9 is finite Element of K19(NAT)

Seg (len (decomp x9)) is non zero finite len (decomp x9) -element Element of K19(NAT)

dom (decomp x9) is finite Element of K19(NAT)

k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

(decomp x9) /. k is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))

u9 /. k is Element of the carrier of O

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*k,b1*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

L . k is Element of the carrier of O

p . b1 is Element of the carrier of O

(L . k) * (p . b1) is Element of the carrier of O

b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b2,k*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

b2 + k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b2,k*> . 2 is set

<*b2,k*> . 1 is set

0. O is zero Element of the carrier of O

0. O is zero Element of the carrier of O

0. O is zero Element of the carrier of O

0. O is zero Element of the carrier of O

<*> the carrier of O is Relation-like NAT -defined the carrier of O -valued Function-like one-to-one constant functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite finite-yielding V34() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V132() ext-real non positive non negative complex V170() V171() V172() V173() FinSequence-yielding finite-support M15( the carrier of O,K256( the carrier of O))

K256( the carrier of O) is functional non zero FinSequence-membered M14( the carrier of O)

the Element of dom u9 is Element of dom u9

k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

u9 /. k is Element of the carrier of O

u9 /. the Element of dom u9 is Element of the carrier of O

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

O is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable V89() right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of O is non zero non trivial set

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

L + p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

x is non zero Element of the carrier of O

x9 is non zero Element of the carrier of O

x * x9 is Element of the carrier of O

Monom ((x * x9),(L + p)) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

K20((Bags n), the carrier of O) is set

K19(K20((Bags n), the carrier of O)) is set

Monom (x,L) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

Monom (x9,p) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

(Monom (x,L)) *' (Monom (x9,p)) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

((Monom (x,L)) *' (Monom (x9,p))) . (L + p) is Element of the carrier of O

decomp (L + p) is Relation-like NAT -defined K257(2,(Bags n)) -valued Function-like one-to-one non zero finite FinSequence-like FinSubsequence-like V132() FinSequence-yielding finite-support FinSequence of K257(2,(Bags n))

K257(2,(Bags n)) is M14( Bags n)

len (decomp (L + p)) is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

b2 is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of O

Sum b2 is Element of the carrier of O

len b2 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

dom b2 is finite Element of K19(NAT)

dom (decomp (L + p)) is finite Element of K19(NAT)

<*L,p*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

b19 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

(decomp (L + p)) /. b19 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))

Seg (len (decomp (L + p))) is non zero finite len (decomp (L + p)) -element Element of K19(NAT)

b2 /. b19 is Element of the carrier of O

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b29,b1*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

(Monom (x,L)) . b29 is Element of the carrier of O

(Monom (x9,p)) . b1 is Element of the carrier of O

((Monom (x,L)) . b29) * ((Monom (x9,p)) . b1) is Element of the carrier of O

<*L,p*> . 1 is set

<*L,p*> . 2 is set

(Monom (x9,p)) . p is Element of the carrier of O

term (Monom (x9,p)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(Monom (x9,p)) . (term (Monom (x9,p))) is Element of the carrier of O

coefficient (Monom (x9,p)) is Element of the carrier of O

0. O is zero Element of the carrier of O

b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(Monom (x9,p)) . b2 is Element of the carrier of O

(Monom (x,L)) . L is Element of the carrier of O

term (Monom (x,L)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(Monom (x,L)) . (term (Monom (x,L))) is Element of the carrier of O

coefficient (Monom (x,L)) is Element of the carrier of O

b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(Monom (x,L)) . b2 is Element of the carrier of O

b2 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

(decomp (L + p)) /. b2 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))

b2 /. b2 is Element of the carrier of O

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

<*b19,b29*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set

(Monom (x,L)) . b19 is Element of the carrier of O

(Monom (x9,p)) . b29 is Element of the carrier of O

((Monom (x,L)) . b19) * ((Monom (x9,p)) . b29) is Element of the carrier of O

(decomp (L + p)) . b2 is FinSequence-like set

(decomp (L + p)) . b19 is FinSequence-like set

term ((Monom (x,L)) *' (Monom (x9,p))) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

term (Monom ((x * x9),(L + p))) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

coefficient ((Monom (x,L)) *' (Monom (x9,p))) is Element of the carrier of O

((Monom (x,L)) *' (Monom (x9,p))) . (term ((Monom (x,L)) *' (Monom (x9,p)))) is Element of the carrier of O

coefficient (Monom ((x * x9),(L + p))) is Element of the carrier of O

Monom ((coefficient (Monom ((x * x9),(L + p)))),(term (Monom ((x * x9),(L + p))))) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

O is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable V89() right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of O is non zero non trivial set

L is Element of the carrier of O

p is Element of the carrier of O

L * p is Element of the carrier of O

(L * p) | (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

K20((Bags n), the carrier of O) is set

K19(K20((Bags n), the carrier of O)) is set

L | (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

p | (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

(L | (n,O)) *' (p | (n,O)) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

term ((L * p) | (n,O)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

coefficient ((L * p) | (n,O)) is Element of the carrier of O

Monom ((L * p),(EmptyBag n)) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

term (p | (n,O)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

coefficient (p | (n,O)) is Element of the carrier of O

Monom (p,(EmptyBag n)) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

term (L | (n,O)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

coefficient (L | (n,O)) is Element of the carrier of O

Monom (L,(EmptyBag n)) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

(EmptyBag n) + (EmptyBag n) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

0. O is zero Element of the carrier of O

0_ (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

0. O is zero Element of the carrier of O

0_ (n,O) is Relation-like Bags n -defined the carrier of O -valued Function-like non zero total V18( Bags n, the carrier of O) monomial-like Constant V235( Bags n,O) Element of K19(K20((Bags n), the carrier of O))

0. O is zero Element of the carrier of O

0. O is zero Element of the carrier of O

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

field O is set

L is set

dom O is functional Element of K19((Bags n))

K19((Bags n)) is set

rng O is functional Element of K19((Bags n))

(dom O) \/ (rng O) is functional Element of K19((Bags n))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

LexOrder n is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) being_linear-order reflexive antisymmetric transitive admissible Element of K19(K20((Bags n),(Bags n)))

L is set

field (LexOrder n) is set

p is set

x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[L,p] is V15() set

[p,L] is V15() set

n is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive admissible Element of K19(K20((Bags n),(Bags n)))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

field O is set

[L,L] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

field O is set

[L,p] is V15() set

[p,L] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

field O is set

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[L,L] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

field O is set

[p,L] is V15() set

[L,p] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

field O is set

[L,p] is V15() set

[L,p] is V15() set

[p,L] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

field O is set

[L,p] is V15() set

[p,x] is V15() set

[L,x] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive admissible Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[(EmptyBag n),L] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive admissible Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

L + x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

[(EmptyBag n),x] is V15() set

(EmptyBag n) + L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[((EmptyBag n) + L),p] is V15() set

[L,p] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,L) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,L) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,p,L) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,p,L) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

(n,O,p,L) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

L is non empty ZeroStr

the carrier of L is non zero set

K20((Bags n), the carrier of L) is set

K19(K20((Bags n), the carrier of L)) is set

p is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

Support p is functional Element of K19((Bags n))

K19((Bags n)) is set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

x9 is finite set

card x9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

card (Support p) is epsilon-transitive epsilon-connected ordinal cardinal set

u9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex set

card u9 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex set

k + 1 is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex set

b1 is functional finite Element of K19((Bags n))

card b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

b2 is functional non zero finite Element of K19((Bags n))

the Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of b2

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

{b29} is functional non zero trivial finite 1 -element set

b2 \ {b29} is functional finite Element of K19((Bags n))

b2 is set

{b29} \/ b2 is non zero finite set

{b29} \/ (b2 \ {b29}) is non zero finite set

card (b2 \ {b29}) is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

(card (b2 \ {b29})) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex set

b2 is non zero set

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

field O is set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[b29,b19] is V15() set

[b29,b19] is V15() set

[b29,b19] is V15() set

[b29,b19] is V15() set

[b19,b19] is V15() set

[b29,b29] is V15() set

[b29,b19] is V15() set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[b29,b19] is V15() set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[b29,b19] is V15() set

[b19,b29] is V15() set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[b29,b29] is V15() set

[b29,b19] is V15() set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[b29,b29] is V15() set

[b29,b19] is V15() set

[b19,b29] is V15() set

[b29,b19] is V15() set

[b19,b29] is V15() set

b29 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

c

c

c

k is functional finite Element of K19((Bags n))

card k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT

{0} is non zero trivial finite V34() 1 -element set

card {0} is non zero epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real positive non negative complex Element of NAT

b1 is set

{b1} is non zero trivial finite 1 -element set

b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

b19 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[b19,k] is V15() set

k is functional finite Element of K19((Bags n))

k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

[b1,k] is V15() set

b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

[x,x9] is V15() set

[x9,x] is V15() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

L is non empty ZeroStr

the carrier of L is non zero set

K20((Bags n), the carrier of L) is set

K19(K20((Bags n), the carrier of L)) is set

p is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

p . (n,O,L,p) is Element of the carrier of L

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

L is non empty ZeroStr

the carrier of L is non zero set

K20((Bags n), the carrier of L) is set

K19(K20((Bags n), the carrier of L)) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

p is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

(n,O,L,p) is Element of the carrier of L

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

p . (n,O,L,p) is Element of the carrier of L

Monom ((n,O,L,p),(n,O,L,p)) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) monomial-like V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is non empty ZeroStr

the carrier of L is non zero set

K20((Bags n), the carrier of L) is set

K19(K20((Bags n), the carrier of L)) is set

0. L is zero Element of the carrier of L

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) monomial-like Constant V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

p is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

(n,O,L,p) is Element of the carrier of L

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

p . (n,O,L,p) is Element of the carrier of L

Support p is functional Element of K19((Bags n))

K19((Bags n)) is set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is non empty non trivial ZeroStr

the carrier of L is non zero non trivial set

K20((Bags n), the carrier of L) is set

K19(K20((Bags n), the carrier of L)) is set

p is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

(n,O,L,p) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) monomial-like V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

(n,O,L,p) is Element of the carrier of L

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

p . (n,O,L,p) is Element of the carrier of L

Monom ((n,O,L,p),(n,O,L,p)) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) monomial-like V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

(n,O,L,p) . (n,O,L,p) is Element of the carrier of L

0. L is zero Element of the carrier of L

term (n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

0. L is zero Element of the carrier of L

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) monomial-like Constant V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

Support p is functional Element of K19((Bags n))

K19((Bags n)) is set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

term (n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

0. L is zero Element of the carrier of L

term (n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

0. L is zero Element of the carrier of L

term (n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set

coefficient (n,O,L,p) is Element of the carrier of L

(n,O,L,p) . (term (n,O,L,p)) is Element of the carrier of L

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K19(K20((Bags n),(Bags n)))

L is non empty non trivial ZeroStr

the carrier of L is non zero non trivial set

K20((Bags n), the carrier of L) is set

K19(K20((Bags n), the carrier of L)) is set

0. L is zero Element of the carrier of L

p is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

(n,O,L,p) is Element of the carrier of L

(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n

p . (n,O,L,p) is Element of the carrier of L

(n,O,L,p) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) monomial-like V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

Monom ((n,O,L,p),(n,O,L,p)) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) monomial-like V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))

Support (n,O,L,p) is functional Element of K19((Bags n))

K19((Bags n)) is set

(n,O,L,p) . (n,O,L,p) is Element of the carrier of L

n is epsilon-transitive epsilon-connected ordinal set

Bags n is functional non zero Element of K19((Bags n))

Bags n is non zero set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((