:: TERMORD semantic presentation

REAL is set

K19(REAL) is set

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

RAT is set
INT is set

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

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

n is set
n is set

p is set

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

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

p is non zero set
{ [b1,((L . b1) -' (O . b1))] where b1 is Element of p : verum } is set
x9 is set
u9 is Element of p

[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

[k,((L . k) -' (O . k))] is V15() set
b1 is Element of p

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

dom x9 is set
k is set
[u9,k] is V15() set
k is Element of p

[k,((L . k) -' (O . k))] is V15() set
u9 is set
k is Element of p

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

k is set
[k,k] is V15() set
b1 is Element of p

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

support u9 is set
dom u9 is Element of K19(p)
K19(p) is set
k is set
u9 . k is set

k is set
rng u9 is set
k is set
[k,k] is V15() set
b1 is Element of p

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

b1 is set

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

(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

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

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))

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

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

Sum x9 is Element of the carrier of O

dom x9 is finite Element of K19(NAT)

x9 /. u9 is Element of the carrier of O

(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

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

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))

p . x is Element of the carrier of O
0. O is zero Element of the carrier of O

p . x9 is Element of the carrier of O

L . x9 is Element of the carrier of O

L . u9 is Element of the carrier of O

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

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

Sum k is Element of the carrier of O

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

k /. b1 is Element of the carrier of O

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,b29*> . 2 is set
<*b19,b29*> . 1 is set

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

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

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

Sum b2 is Element of the carrier of O

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)

b2 /. k is Element of the carrier of O

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,b2*> . 2 is set
<*b1,b2*> . 1 is set

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

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

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

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))

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

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

Sum u9 is Element of the carrier of O

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)

u9 /. k is Element of the carrier of O

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,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

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

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

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

the carrier of O is non zero non trivial 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

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

Sum b2 is Element of the carrier of O

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

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

(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

(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

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

(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

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

b2 /. b2 is Element of the carrier of O

(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))

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

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

coefficient ((L * p) | (n,O)) is Element of the carrier of O
Monom ((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))

coefficient (p | (n,O)) is Element of the carrier of O
Monom (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))

coefficient (L | (n,O)) is Element of the carrier of O
Monom (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))

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

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

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))

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 set
field () is set
p is set

[L,p] is V15() set
[p,L] is V15() 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

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

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

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

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

field O is set
[L,L] is V15() 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

field O is set
[L,p] is V15() set
[p,L] is V15() 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

field O is set

[L,L] is V15() 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

field O is set
[p,L] is V15() set
[L,p] is V15() 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

field O is set
[L,p] is V15() set
[L,p] is V15() set
[p,L] is V15() 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

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

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

field O is set
[L,p] is V15() set
[p,x] is V15() set
[L,x] is V15() 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 V15() 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

[(),x] is V15() set

[(() + L),p] is V15() set
[L,p] is V15() 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,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support 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,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support 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,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

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,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support 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,O,L,p) is Relation-like n -defined RAT -valued Function-like total V170() V171() V172() V173() finite-support 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,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

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,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

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

x9 is finite set

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

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

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

b2 is non zero set

field O is 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,b19] is V15() set

[b29,b19] is V15() set
[b19,b29] is V15() set

[b29,b29] is V15() set
[b29,b19] is V15() 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

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

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

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

[b19,k] is V15() set
k is functional finite Element of K19((Bags n))

[b1,k] is V15() set

[x,x9] is V15() set
[x9,x] is V15() 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))

(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

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))
(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))

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
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

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
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

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

0. L is zero Element of the carrier of L

0. L is zero Element of the carrier of L

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

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
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

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((