:: 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₁,((L . b₁) -' (O . b₁))] where b₁ is Element of p : verum } is set
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₁₉ is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
c₁₉ is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
c₂₀ is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
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((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
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))
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
{(term (n,O,L,p))} is functional non zero trivial finite 1 -element set
(n,O,L,p) . (EmptyBag n) 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 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
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) non-zero 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))
0. L is zero Element of the carrier of L
Support (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
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))
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))
0. L is zero Element of the carrier of L
0. L is zero Element of the carrier of L
0. L is zero Element of the carrier of L
Support p is functional Element of K19((Bags n))
K19((Bags n)) is set
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))
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
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 Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
term p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(n,O,L,p) is Element of the carrier of L
p . (n,O,L,p) is Element of the carrier of L
coefficient 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 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
Support p is functional Element of K19((Bags n))
K19((Bags n)) is set
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
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 L
0. L is zero Element of the carrier of L
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
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
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
x is epsilon-transitive epsilon-connected ordinal set
Bags x is functional non zero Element of K19((Bags x))
Bags x is non zero set
K19((Bags x)) is set
K20((Bags x),(Bags x)) is set
K19(K20((Bags x),(Bags x))) is set
u9 is non empty ZeroStr
the carrier of u9 is non zero set
K20((Bags x), the carrier of u9) is set
K19(K20((Bags x), the carrier of u9)) 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
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))
k is Relation-like Bags x -defined the carrier of u9 -valued Function-like non zero total V18( Bags x, the carrier of u9) V235( Bags x,u9) Element of K19(K20((Bags x), the carrier of u9))
0_ (x,u9) is Relation-like Bags x -defined the carrier of u9 -valued Function-like non zero total V18( Bags x, the carrier of u9) monomial-like Constant V235( Bags x,u9) Element of K19(K20((Bags x), the carrier of u9))
x9 is Relation-like Bags x -defined Bags x -valued total V18( Bags x, Bags x) reflexive antisymmetric connected transitive Element of K19(K20((Bags x),(Bags x)))
(x,x9,u9,k) is Element of the carrier of u9
(x,x9,u9,k) is Relation-like x -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags x
k . (x,x9,u9,k) is Element of the carrier of u9
0. u9 is zero Element of the carrier of u9
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 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
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 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
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 Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(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
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))
x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(n,O,L,p) . x is Element of the carrier of L
Support (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
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 (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
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
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
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 (n,O,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
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))
Support (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
0. L is zero Element of the carrier of L
0. L is zero Element of the carrier of L
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
0. L is zero Element of the carrier of L
0. L is zero 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
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))
Support (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
Support p is functional Element of K19((Bags n))
x is set
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
0. L is zero Element of 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
0. L is zero Element of the carrier of L
0. L is zero Element of the carrier of L
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
{(n,O,L,p)} is functional non zero trivial finite 1 -element 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 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
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 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))
Support (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
{(n,O,L,p)} is functional non zero trivial finite 1 -element 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))
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
x is non zero Element of the carrier of L
Monom (x,(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))
term (Monom (x,(n,O,L,p))) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
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
0. L is zero Element of the carrier of L
Monom ((0. 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))
term (Monom ((0. L),(n,O,L,p))) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
x is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(n,O,L,x) is non zero Element of the carrier of L
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
x . (n,O,L,x) 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
x is epsilon-transitive epsilon-connected ordinal set
Bags x is functional non zero Element of K19((Bags x))
Bags x is non zero set
K19((Bags x)) is set
K20((Bags x),(Bags x)) is set
K19(K20((Bags x),(Bags x))) is set
u9 is non empty ZeroStr
the carrier of u9 is non zero set
K20((Bags x), the carrier of u9) is set
K19(K20((Bags x), the carrier of u9)) is set
k is epsilon-transitive epsilon-connected ordinal set
Bags k is functional non zero Element of K19((Bags k))
Bags k is non zero set
K19((Bags k)) is set
K20((Bags k),(Bags k)) is set
K19(K20((Bags k),(Bags k))) is set
b2 is non empty ZeroStr
the carrier of b2 is non zero set
K20((Bags k), the carrier of b2) is set
K19(K20((Bags k), the carrier of b2)) 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) monomial-like V235( Bags n,L) Element of K19(K20((Bags n), 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
term p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
x9 is Relation-like Bags x -defined Bags x -valued total V18( Bags x, Bags x) reflexive antisymmetric connected transitive Element of K19(K20((Bags x),(Bags x)))
k is Relation-like Bags x -defined the carrier of u9 -valued Function-like non zero total V18( Bags x, the carrier of u9) monomial-like V235( Bags x,u9) Element of K19(K20((Bags x), the carrier of u9))
(x,x9,u9,k) is Element of the carrier of u9
(x,x9,u9,k) is Relation-like x -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags x
k . (x,x9,u9,k) is Element of the carrier of u9
coefficient k is Element of the carrier of u9
b1 is Relation-like Bags k -defined Bags k -valued total V18( Bags k, Bags k) reflexive antisymmetric connected transitive Element of K19(K20((Bags k),(Bags k)))
k is Relation-like Bags k -defined the carrier of b2 -valued Function-like non zero total V18( Bags k, the carrier of b2) monomial-like V235( Bags k,b2) Element of K19(K20((Bags k), the carrier of b2))
(k,b1,b2,k) is Relation-like Bags k -defined the carrier of b2 -valued Function-like non zero total V18( Bags k, the carrier of b2) monomial-like V235( Bags k,b2) Element of K19(K20((Bags k), the carrier of b2))
(k,b1,b2,k) is Element of the carrier of b2
(k,b1,b2,k) is Relation-like k -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags k
k . (k,b1,b2,k) is Element of the carrier of b2
Monom ((k,b1,b2,k),(k,b1,b2,k)) is Relation-like Bags k -defined the carrier of b2 -valued Function-like non zero total V18( Bags k, the carrier of b2) monomial-like V235( Bags k,b2) Element of K19(K20((Bags k), the carrier of b2))
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 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
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 Constant V235( Bags n,L) Element of K19(K20((Bags n), 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
(n,O,L,p) is Element of the carrier of L
p . (n,O,L,p) is Element of the carrier of L
p . (EmptyBag n) is Element of the carrier of L
term p is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
coefficient 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
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)))
L is non empty ZeroStr
the carrier of L is non zero set
p is Element of the carrier of L
p | (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))
K20((Bags n), the carrier of L) is set
K19(K20((Bags n), the carrier of L)) is set
(n,O,L,(p | (n,L))) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(n,O,L,(p | (n,L))) is Element of the carrier of L
(p | (n,L)) . (n,O,L,(p | (n,L))) is Element of the carrier of L
term (p | (n,L)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
coefficient (p | (n,L)) 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
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,(n,O,L,p)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
x is non zero Element of the carrier of L
Monom (x,(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))
term (Monom (x,(n,O,L,p))) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
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
0. L is zero Element of the carrier of L
Monom ((0. 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))
term (Monom ((0. L),(n,O,L,p))) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
term (n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
x is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(n,O,L,x) is non zero Element of the carrier of L
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
x . (n,O,L,x) 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
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,(n,O,L,p)) is Element of the carrier of L
(n,O,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
(n,O,L,p) . (n,O,L,(n,O,L,p)) is Element of the carrier of L
(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((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 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,(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,(n,O,L,p)) is Element of the carrier of L
(n,O,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
(n,O,L,p) . (n,O,L,(n,O,L,p)) is Element of the carrier of L
Monom ((n,O,L,(n,O,L,p)),(n,O,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 is set
K19(n) is set
K20(n,n) is set
K19(K20(n,n)) is set
O is Element of K19(n)
L is Relation-like n -defined n -valued total V18(n,n) reflexive antisymmetric transitive Element of K19(K20(n,n))
field L 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 admissible Element of K19(K20((Bags n),(Bags n)))
L 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 left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
x is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
p *' x 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 n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(n,O,L,p) + (n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(p *' x) . ((n,O,L,p) + (n,O,L,x)) is Element of the carrier of L
p . (n,O,L,p) is Element of the carrier of L
x . (n,O,L,x) is Element of the carrier of L
(p . (n,O,L,p)) * (x . (n,O,L,x)) is Element of the carrier of L
decomp ((n,O,L,p) + (n,O,L,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 ((n,O,L,p) + (n,O,L,x))) 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 L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum u9 is Element of the carrier of L
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)
K19((Bags n)) is set
divisors ((n,O,L,p) + (n,O,L,x)) is Relation-like NAT -defined Bags n -valued Function-like one-to-one non zero finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags n
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)))
k is functional non zero finite Element of K19((Bags n))
SgmX ((LexOrder n),k) is Relation-like NAT -defined Bags n -valued Function-like one-to-one non zero finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags n
rng (SgmX ((LexOrder n),k)) is finite set
dom (SgmX ((LexOrder n),k)) is finite Element of K19(NAT)
b1 is set
(SgmX ((LexOrder n),k)) . b1 is Relation-like Function-like set
dom (decomp ((n,O,L,p) + (n,O,L,x))) is finite Element of K19(NAT)
(divisors ((n,O,L,p) + (n,O,L,x))) /. b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(decomp ((n,O,L,p) + (n,O,L,x))) /. b1 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))
((n,O,L,p) + (n,O,L,x)) -' (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),(((n,O,L,p) + (n,O,L,x)) -' (n,O,L,p))*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set
<*(n,O,L,p),(n,O,L,x)*> is Relation-like NAT -defined Bags n -valued Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support M15( Bags n,K256((Bags n)))
K256((Bags n)) is functional non zero FinSequence-membered M14( Bags n)
Seg (len (decomp ((n,O,L,p) + (n,O,L,x)))) is non zero finite len (decomp ((n,O,L,p) + (n,O,L,x))) -element Element of K19(NAT)
b2 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT
(decomp ((n,O,L,p) + (n,O,L,x))) /. b2 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))
u9 /. b2 is Element of the carrier of L
k 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
<*k,b19*> is Relation-like NAT -defined Function-like non zero finite 2 -element FinSequence-like FinSubsequence-like finite-support set
p . k is Element of the carrier of L
x . b19 is Element of the carrier of L
(p . k) * (x . b19) is Element of the carrier of L
<*(n,O,L,p),(n,O,L,x)*> . 2 is Relation-like Function-like set
b29 is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT
(decomp ((n,O,L,p) + (n,O,L,x))) /. b29 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))
u9 /. b29 is Element of the carrier of L
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
p . b1 is Element of the carrier of L
x . b2 is Element of the carrier of L
(p . b1) * (x . b2) is Element of the carrier of L
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
0. L is zero Element of the carrier of L
Support p is functional finite Element of K19((Bags n))
[b1,(n,O,L,p)] is V15() set
Support x is functional finite Element of K19((Bags n))
[b2,(n,O,L,x)] is V15() set
(decomp ((n,O,L,p) + (n,O,L,x))) . b29 is FinSequence-like set
(decomp ((n,O,L,p) + (n,O,L,x))) . b2 is FinSequence-like set
b1 + b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(n,O,L,p) + b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
((n,O,L,p) + b2) -' b2 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
[((n,O,L,p) + (n,O,L,x)),((n,O,L,p) + b2)] is V15() set
[((n,O,L,p) + b2),((n,O,L,p) + (n,O,L,x))] is V15() set
b2 + b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(n,O,L,x) + b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
((n,O,L,x) + b1) -' b1 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
[((n,O,L,p) + (n,O,L,x)),((n,O,L,x) + b1)] is V15() set
[((n,O,L,x) + b1),((n,O,L,p) + (n,O,L,x))] is V15() set
<*(n,O,L,p),(n,O,L,x)*> . 1 is Relation-like Function-like 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 admissible Element of K19(K20((Bags n),(Bags n)))
L 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 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) non-zero V235( Bags n,L) Element of K19(K20((Bags n), 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
x is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(n,O,L,p) + (n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
p *' x 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 *' x) is functional finite Element of K19((Bags n))
K19((Bags n)) is set
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 finite Element of K19((Bags n))
p . (n,O,L,p) is Element of the carrier of L
0. L is zero Element of the carrier of L
Support x is functional finite Element of K19((Bags n))
x . (n,O,L,x) is Element of the carrier of L
(p *' x) . ((n,O,L,p) + (n,O,L,x)) is Element of the carrier of L
(p . (n,O,L,p)) * (x . (n,O,L,x)) 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
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) 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) 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 is functional Element of K19((Bags n))
Support p is functional Element of K19((Bags n))
{ (b₁ + b₂) where b₁, b₂ is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n : ( b₁ in Support L & b₂ in Support p ) } is set
x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(L *' p) . 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)
Seg (len (decomp x)) is non zero finite len (decomp x) -element Element of K19(NAT)
dom (decomp x) is finite Element of K19(NAT)
Seg (len x9) is finite len x9 -element Element of K19(NAT)
the Element of dom x9 is Element of dom x9
0. O is zero Element of the carrier of O
k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex set
x9 /. k is Element of the carrier of O
(decomp x) /. k is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))
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
L . b1 is Element of the carrier of O
p . b2 is Element of the carrier of O
(L . b1) * (p . b2) is Element of the carrier of O
k 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 Element of NAT
x9 /. k is Element of the carrier of O
x9 /. k is Element of the carrier of O
k is Element of dom (decomp x)
(decomp x) /. k is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))
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
L . b1 is Element of the carrier of O
p . b2 is Element of the carrier of O
k is Element of dom (decomp x)
(decomp x) /. k is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))
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
L . b1 is Element of the carrier of O
p . b2 is Element of the carrier of O
k is epsilon-transitive epsilon-connected ordinal natural V28() finite cardinal ext-real non negative complex Element of NAT
(decomp x) /. k is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K257(2,(Bags n))
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
<*b1,b2*> . 2 is set
<*b1,b2*> . 1 is set
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
u9 + k is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
x is set
x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
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
u9 + k 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 admissible Element of K19(K20((Bags n),(Bags n)))
L 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 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) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
x is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
p *' x 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 *' x)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of 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
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(n,O,L,p) + (n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
Support (p *' x) is functional finite Element of K19((Bags n))
K19((Bags n)) is set
[((n,O,L,p) + (n,O,L,x)),(n,O,L,(p *' x))] is V15() set
Support p is functional finite Element of K19((Bags n))
Support x is functional finite Element of K19((Bags n))
{ (b₁ + b₂) where b₁, b₂ is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n : ( b₁ in Support p & b₂ in Support x ) } is set
x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
x9 + u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
[x9,(n,O,L,p)] is V15() set
(n,O,L,p) + u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
[(x9 + u9),((n,O,L,p) + u9)] is V15() set
[u9,(n,O,L,x)] is V15() set
u9 + (n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
[(u9 + (n,O,L,p)),((n,O,L,p) + (n,O,L,x))] is V15() set
[(x9 + u9),((n,O,L,p) + (n,O,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
O is Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive admissible Element of K19(K20((Bags n),(Bags n)))
L 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 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) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
x is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
p *' x 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 *' x)) is Element of the carrier of L
(n,O,L,(p *' x)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(p *' x) . (n,O,L,(p *' x)) is Element of the carrier of L
(n,O,L,p) is non zero 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,x) is non zero Element of the carrier of L
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
x . (n,O,L,x) is Element of the carrier of L
(n,O,L,p) * (n,O,L,x) is Element of the carrier of L
(n,O,L,p) + (n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(p *' x) . ((n,O,L,p) + (n,O,L,x)) 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 admissible Element of K19(K20((Bags n),(Bags n)))
L 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 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) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
x is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
p *' x 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 *' x)) 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 *' x)) is Element of the carrier of L
(n,O,L,(p *' x)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(p *' x) . (n,O,L,(p *' x)) is Element of the carrier of L
Monom ((n,O,L,(p *' x)),(n,O,L,(p *' x))) 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 Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero monomial-like V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(n,O,L,p) is non zero 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,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non zero total V18( Bags n, the carrier of L) non-zero monomial-like V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(n,O,L,x) is non zero Element of the carrier of L
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
x . (n,O,L,x) is Element of the carrier of L
Monom ((n,O,L,x),(n,O,L,x)) 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,x) 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,x) is Element of the carrier of L
Monom (((n,O,L,p) * (n,O,L,x)),(n,O,L,(p *' x))) 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,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
Monom (((n,O,L,p) * (n,O,L,x)),((n,O,L,p) + (n,O,L,x))) 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 admissible Element of K19(K20((Bags n),(Bags n)))
L is non empty right_zeroed addLoopStr
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))
x 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))
p + x 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 + x)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of 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
(n,O,L,x) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(n,O,(n,O,L,p),(n,O,L,x)) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
Support (p + x) is functional Element of K19((Bags n))
K19((Bags n)) is set
Support p is functional Element of K19((Bags n))
Support x is functional Element of K19((Bags n))
(Support p) \/ (Support x) is functional Element of K19((Bags n))
Support (p + x) 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
[(n,O,L,(p + x)),(n,O,(n,O,L,p),(n,O,L,x))] is V15() set
Support (p + x) 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
L is non empty left_add-cancelable right_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 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 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))
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) 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 non trivial left_add-cancelable right_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 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 n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(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) 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
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))
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) 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
0. L is zero Element of the carrier of L
- (n,O,L,p) is Relation-like Bags n -defined Bags n -defined the carrier of L -valued Function-like non zero total total V18( Bags n, the carrier of L) V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of 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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(p + (- (n,O,L,p))) . (n,O,L,p) is Element of the carrier of L
(- (n,O,L,p)) . (n,O,L,p) is Element of the carrier of L
(p . (n,O,L,p)) + ((- (n,O,L,p)) . (n,O,L,p)) is Element of the carrier of L
(n,O,L,p) . (n,O,L,p) is Element of the carrier of L
- ((n,O,L,p) . (n,O,L,p)) is Element of the carrier of L
(p . (n,O,L,p)) + (- ((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((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 left_add-cancelable right_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 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))
Support p is functional Element of K19((Bags n))
K19((Bags n)) is set
(n,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(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) 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
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))
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) 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))
x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(n,O,L,p) . x is Element of the carrier of L
- (n,O,L,p) is Relation-like Bags n -defined Bags n -defined the carrier of L -valued Function-like non zero total total V18( Bags n, the carrier of L) V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of 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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(p + (- (n,O,L,p))) . x is Element of the carrier of L
p . x is Element of the carrier of L
(- (n,O,L,p)) . x is Element of the carrier of L
(p . x) + ((- (n,O,L,p)) . x) is Element of the carrier of L
(n,O,L,p) . x is Element of the carrier of L
- ((n,O,L,p) . x) is Element of the carrier of L
(p . x) + (- ((n,O,L,p) . x)) is Element of the carrier of L
0. L is zero Element of the carrier of L
- (0. L) is Element of the carrier of L
(p . x) + (- (0. L)) is Element of the carrier of L
(p . x) + (0. L) 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 left_add-cancelable right_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 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) 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))
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) 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
Support p is functional Element of K19((Bags n))
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
(Support p) \ {(n,O,L,p)} is functional Element of K19((Bags n))
x is set
x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(p - (n,O,L,p)) . u9 is Element of the carrier of L
0. L is zero Element of the carrier of L
- (n,O,L,p) is Relation-like Bags n -defined Bags n -defined the carrier of L -valued Function-like non zero total total V18( Bags n, the carrier of L) V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of 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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(p + (- (n,O,L,p))) . u9 is Element of the carrier of L
p . u9 is Element of the carrier of L
(- (n,O,L,p)) . u9 is Element of the carrier of L
(p . u9) + ((- (n,O,L,p)) . u9) is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
- ((n,O,L,p) . u9) is Element of the carrier of L
(p . u9) + (- ((n,O,L,p) . u9)) is Element of the carrier of L
- (0. L) is Element of the carrier of L
(p . u9) + (- (0. L)) is Element of the carrier of L
(p . u9) + (0. L) is Element of the carrier of L
x is set
x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
u9 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 non empty non trivial left_add-cancelable right_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 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) 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))
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) 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
Support p is functional Element of K19((Bags n))
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
(Support p) \ {(n,O,L,p)} 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
L is non empty non trivial left_add-cancelable right_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 zero non trivial 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 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))
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) 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
Support p is functional Element of K19((Bags n))
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
(Support p) \ {(n,O,L,p)} 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
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 left_add-cancelable right_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 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 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))
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) 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
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
Support (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
Support p is functional Element of K19((Bags n))
(Support p) \ {(n,O,L,p)} 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
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 left_add-cancelable right_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 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 n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
(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) 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
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))
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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
(n,O,L,p) . x is Element of the carrier of L
p . x is Element of the carrier of L
{(n,O,L,p)} is functional non zero trivial finite 1 -element set
Support (n,O,L,p) is functional Element of K19((Bags n))
K19((Bags n)) is set
- (n,O,L,p) is Relation-like Bags n -defined Bags n -defined the carrier of L -valued Function-like non zero total total V18( Bags n, the carrier of L) V18( Bags n, the carrier of L) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of 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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(p + (- (n,O,L,p))) . x is Element of the carrier of L
(- (n,O,L,p)) . x is Element of the carrier of L
(p . x) + ((- (n,O,L,p)) . x) is Element of the carrier of L
(n,O,L,p) . x is Element of the carrier of L
- ((n,O,L,p) . x) is Element of the carrier of L
(p . x) + (- ((n,O,L,p) . x)) is Element of the carrier of L
0. L is zero Element of the carrier of L
- (0. L) is Element of the carrier of L
(p . x) + (- (0. L)) is Element of the carrier of L
(p . x) + (0. L) 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 left_add-cancelable right_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 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) 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))
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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
Support ((n,O,L,p) + (n,O,L,p)) is functional Element of K19((Bags n))
K19((Bags n)) is set
Support p is functional Element of K19((Bags n))
x is set
x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
p . u9 is Element of the carrier of L
0. L is zero Element of the carrier of L
((n,O,L,p) + (n,O,L,p)) . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
((n,O,L,p) . u9) + ((n,O,L,p) . u9) is Element of the carrier of L
((n,O,L,p) . u9) + (0. L) is Element of the carrier of L
((n,O,L,p) + (n,O,L,p)) . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
((n,O,L,p) . u9) + ((n,O,L,p) . u9) is Element of the carrier of L
((n,O,L,p) . u9) + (p . u9) is Element of the carrier of L
(0. L) + (p . u9) is Element of the carrier of L
x is set
x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
u9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support set
((n,O,L,p) + (n,O,L,p)) . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
((n,O,L,p) . u9) + ((n,O,L,p) . u9) is Element of the carrier of L
(n,O,L,p) . (n,O,L,p) is Element of the carrier of L
((n,O,L,p) . (n,O,L,p)) + (0. L) is Element of the carrier of L
p . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
(n,O,L,p) . u9 is Element of the carrier of L
((n,O,L,p) . u9) + ((n,O,L,p) . u9) is Element of the carrier of L
(0. L) + ((n,O,L,p) . u9) is Element of the carrier of L
p . x 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 left_add-cancelable right_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 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) 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))
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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
x is set
((n,O,L,p) + (n,O,L,p)) . x is set
(n,O,L,p) . (n,O,L,p) is Element of the carrier of L
(n,O,L,p) . (n,O,L,p) is Element of the carrier of L
((n,O,L,p) . (n,O,L,p)) + ((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
((n,O,L,p) . (n,O,L,p)) + (0. L) is Element of the carrier of L
p . x is set
x9 is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support Element of Bags n
((n,O,L,p) + (n,O,L,p)) . x9 is Element of the carrier of L
(n,O,L,p) . x9 is Element of the carrier of L
(n,O,L,p) . x9 is Element of the carrier of L
((n,O,L,p) . x9) + ((n,O,L,p) . x9) is Element of the carrier of L
p . x9 is Element of the carrier of L
((n,O,L,p) . x9) + (p . x9) is Element of the carrier of L
0. L is zero Element of the carrier of L
(0. L) + (p . x9) is Element of the carrier of L
p . x is set
((n,O,L,p) + (n,O,L,p)) . x is set
((n,O,L,p) + (n,O,L,p)) . x is set
p . x is set
((n,O,L,p) + (n,O,L,p)) . x is set
p . x is set
dom p is functional Element of K19((Bags n))
K19((Bags n)) is set
dom ((n,O,L,p) + (n,O,L,p)) 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
L is non empty non trivial left_add-cancelable right_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 zero non trivial 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 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))
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) 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
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 non trivial left_add-cancelable right_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 zero non trivial set
K20((Bags n), the carrier of L) is set
K19(K20((Bags n), the carrier of L)) is set
x is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support 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
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
(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) 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
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))
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) V235( Bags n,L) Element of K19(K20((Bags n), the carrier of L))
(n,O,L,p) . x is Element of the carrier of L
p . x is Element of the carrier of L