:: POLYRED semantic presentation

REAL is set

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

bool REAL is cup-closed diff-closed preBoolean set

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

bool NAT is non trivial non finite cup-closed diff-closed preBoolean set

bool NAT is non trivial non finite cup-closed diff-closed preBoolean set

COMPLEX is set

RAT is set

INT is set

0 is zero Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V28() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V49() V135() ext-real non positive non negative complex irreflexive V242() V243() V244() V245() FinSequence-yielding finite-support set

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

{0,1} is non zero finite V28() set

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

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is cup-closed diff-closed preBoolean set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is cup-closed diff-closed preBoolean set

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is cup-closed diff-closed preBoolean set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is cup-closed diff-closed preBoolean set

[:RAT,RAT:] is Relation-like set

bool [:RAT,RAT:] is cup-closed diff-closed preBoolean set

[:[:RAT,RAT:],RAT:] is Relation-like set

bool [:[:RAT,RAT:],RAT:] is cup-closed diff-closed preBoolean set

[:INT,INT:] is Relation-like set

bool [:INT,INT:] is cup-closed diff-closed preBoolean set

[:[:INT,INT:],INT:] is Relation-like set

bool [:[:INT,INT:],INT:] is cup-closed diff-closed preBoolean set

[:NAT,NAT:] is non trivial Relation-like non finite set

[:[:NAT,NAT:],NAT:] is non trivial Relation-like non finite set

bool [:[:NAT,NAT:],NAT:] is non trivial non finite cup-closed diff-closed preBoolean set

[:NAT,REAL:] is Relation-like set

bool [:NAT,REAL:] is cup-closed diff-closed preBoolean set

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

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

Seg 1 is non zero trivial finite 1 -element Element of bool NAT

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

Seg 2 is non zero finite 2 -element Element of bool NAT

{1,2} is non zero finite V28() set

0 is zero Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V28() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V49() V135() ext-real non positive non negative complex irreflexive V242() V243() V244() V245() FinSequence-yielding finite-support Element of NAT

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty non trivial ZeroStr

the carrier of T is non zero non trivial set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

NonZero T is non zero Element of bool the carrier of T

bool the carrier of T is cup-closed diff-closed preBoolean set

[#] T is non zero non proper Element of bool the carrier of T

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

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

([#] T) \ {(0. T)} is Element of bool the carrier of T

the Element of NonZero T is Element of NonZero T

P is Element of the carrier of T

P | (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

f is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

(0. T) | (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

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

n is set

bool n is cup-closed diff-closed preBoolean set

[:n,n:] is Relation-like set

bool [:n,n:] is cup-closed diff-closed preBoolean set

T is Element of bool n

L is Relation-like n -defined n -valued total V46(n,n) reflexive antisymmetric transitive Element of bool [:n,n:]

field L is set

n is epsilon-transitive epsilon-connected ordinal set

T is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

T + P is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

L + P is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

f is epsilon-transitive epsilon-connected ordinal set

L . f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

T . f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

g is epsilon-transitive epsilon-connected ordinal set

(T + P) . g is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

T . g is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

P . g is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

(T . g) + (P . g) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex set

L . g is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

(L . g) + (P . g) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex set

(L + P) . g is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

(T + P) . f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

P . f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

(T . f) + (P . f) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex set

(L + P) . f is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

(L . f) + (P . f) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex set

n is epsilon-transitive epsilon-connected ordinal set

T is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

T is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

P is epsilon-transitive epsilon-connected ordinal set

L . P is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

T . P is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex V241() set

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty non trivial ZeroStr

the carrier of T is non zero non trivial set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) non-zero finite-Support Element of bool [:(Bags n), the carrier of T:]

bool (Bags n) is cup-closed diff-closed preBoolean set

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

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

f is functional finite Element of bool (Bags n)

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

g is non zero functional finite Element of bool (Bags n)

the Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of g

g9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

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

g \ {f9} is functional finite Element of bool (Bags n)

R is set

{f9} \/ g is non zero finite set

{f9} \/ (g \ {f9}) is non zero finite set

card (g \ {f9}) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex Element of NAT

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

R is non zero set

x is non zero functional finite Element of bool (Bags n)

x is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

q is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

q is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

q is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

q is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

Support L is functional Element of bool (Bags n)

P is finite set

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

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

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

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

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

g is functional finite Element of bool (Bags n)

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

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

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

f9 is set

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

g9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

g9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

L . f9 is Element of the carrier of T

L . g is Element of the carrier of T

n is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of n is non zero set

T is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

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

L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

Sum L is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

T /. (len T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

(Sum L) + (T /. (len T)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

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

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

Seg P is finite P -element Element of bool NAT

T | (Seg P) is Relation-like NAT -defined Seg P -defined NAT -defined the carrier of n -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT, the carrier of n:]

[:NAT, the carrier of n:] is non trivial Relation-like non finite set

bool [:NAT, the carrier of n:] is non trivial non finite cup-closed diff-closed preBoolean set

<*(T /. (len T))*> is non zero trivial Relation-like NAT -defined the carrier of n -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support M30( the carrier of n,K500( the carrier of n))

K500( the carrier of n) is non zero functional FinSequence-membered M29( the carrier of n)

L ^ <*(T /. (len T))*> is non zero Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len <*(T /. (len T))*> is non zero epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real positive non negative complex Element of NAT

dom T is finite Element of bool NAT

Seg (P + 1) is non zero finite P + 1 -element K216(P,1) -element Element of bool NAT

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

f9 is set

{ b

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

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

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

(len L) + (len <*(T /. (len T))*>) is non zero epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real positive non negative complex set

(L ^ <*(T /. (len T))*>) . g9 is set

g9 - (len L) is V49() ext-real complex set

<*(T /. (len T))*> . (g9 - (len L)) is set

(P + 1) - P is V49() ext-real complex set

<*(T /. (len T))*> . ((P + 1) - P) is set

<*(T /. (len T))*> . 1 is set

T /. (P + 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

T . g9 is set

{ b

dom L is finite Element of bool NAT

(L ^ <*(T /. (len T))*>) . g9 is set

L . g9 is set

T . g9 is set

(L ^ <*(T /. (len T))*>) . g9 is set

T . g9 is set

(L ^ <*(T /. (len T))*>) . g9 is set

T . g9 is set

T . f9 is set

(L ^ <*(T /. (len T))*>) . f9 is set

len (L ^ <*(T /. (len T))*>) is non zero epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real positive non negative complex Element of NAT

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

(len L) + (len <*(T /. (len T))*>) is non zero epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real positive non negative complex set

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

Seg (len (L ^ <*(T /. (len T))*>)) is non zero finite len (L ^ <*(T /. (len T))*>) -element Element of bool NAT

dom (L ^ <*(T /. (len T))*>) is non zero finite Element of bool NAT

Sum <*(T /. (len T))*> is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

(Sum L) + (Sum <*(T /. (len T))*>) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable V102() 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 T is non zero non trivial set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) non-zero finite-Support Element of bool [:(Bags n), the carrier of T:]

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) non-zero finite-Support Element of bool [:(Bags n), the carrier of T:]

L *' P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

0. T is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

P . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

L . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

g + f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(L *' P) . (g + f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

decomp (g + f) is non zero Relation-like NAT -defined K501(2,(Bags n)) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V135() FinSequence-yielding finite-support FinSequence of K501(2,(Bags n))

K501(2,(Bags n)) is M29( Bags n)

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

g9 is Relation-like NAT -defined the carrier of T -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of T

Sum g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

dom g9 is finite Element of bool NAT

(L . g) * (P . f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

bool (Bags n) is cup-closed diff-closed preBoolean set

divisors (g + f) is non zero Relation-like NAT -defined Bags n -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags n

LexOrder n is Relation-like Bags n -defined Bags n -valued total V46( Bags n, Bags n) being_linear-order reflexive antisymmetric transitive admissible Element of bool [:(Bags n),(Bags n):]

[:(Bags n),(Bags n):] is Relation-like set

bool [:(Bags n),(Bags n):] is cup-closed diff-closed preBoolean set

f9 is non zero functional finite Element of bool (Bags n)

SgmX ((LexOrder n),f9) is non zero Relation-like NAT -defined Bags n -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags n

rng (SgmX ((LexOrder n),f9)) is non zero finite set

dom (SgmX ((LexOrder n),f9)) is non zero finite Element of bool NAT

R is set

(SgmX ((LexOrder n),f9)) . R is Relation-like Function-like set

dom (decomp (g + f)) is non zero finite Element of bool NAT

(divisors (g + f)) /. R is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

(decomp (g + f)) /. R is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K501(2,(Bags n))

(g + f) -' g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

<*g,((g + f) -' g)*> is non zero Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like finite-support set

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

Seg (len (decomp (g + f))) is non zero finite len (decomp (g + f)) -element Element of bool NAT

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

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

g9 /. x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

x is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

q is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

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

L . x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . x) * (P . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

<*g,f*> . 2 is set

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

(decomp (g + f)) /. u is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K501(2,(Bags n))

g9 /. u is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

a is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

u9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

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

L . a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P . u9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . a) * (P . u9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

a9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

u9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

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

a9 + u9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

<*a9,u9*> . 2 is set

<*a9,u9*> . 1 is set

(decomp (g + f)) . u is FinSequence-like set

(decomp (g + f)) . x is FinSequence-like set

a + u9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

g + u9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(g + u9) -' u9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

u9 + a is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

f + a is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(f + a) -' a is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

<*g,f*> . 1 is set

Support (L *' P) is functional finite Element of bool (Bags n)

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

L + P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

- (L + P) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

- L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

- P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

(- L) + (- P) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f is set

dom (- (L + P)) is non zero functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

((- L) + (- P)) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- L) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- P) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

((- L) . g) + ((- P) . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (L . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (L . g)) + ((- P) . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (P . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (L . g)) + (- (P . g)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(P . g) + (L . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- ((P . g) + (L . g)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L + P) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- ((L + P) . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (L + P)) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (L + P)) . f is set

((- L) + (- P)) . f is set

dom ((- L) + (- P)) is non zero functional Element of bool (Bags n)

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_zeroed addLoopStr

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

(0_ (n,T)) + L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

P . g is Element of the carrier of T

(0_ (n,T)) . g is Element of the carrier of T

L . g is Element of the carrier of T

((0_ (n,T)) . g) + (L . g) is Element of the carrier of T

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

f is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f . g is Element of the carrier of T

(0. T) + (f . g) is Element of the carrier of T

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

- L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

(- L) + L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

L + (- L) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

((- L) + L) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- L) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

((- L) . f) + (L . f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (L . f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (L . f)) + (L . f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

0. T is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(0_ (n,T)) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

(L + (- L)) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- L) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . g) + ((- L) . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (L . g) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . g) + (- (L . g)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(0_ (n,T)) . g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

L - (0_ (n,T)) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

P . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (0_ (n,T)) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

L + (- (0_ (n,T))) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

(L + (- (0_ (n,T)))) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (0_ (n,T))) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . f) + ((- (0_ (n,T))) . f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(0_ (n,T)) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- ((0_ (n,T)) . f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . f) + (- ((0_ (n,T)) . f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

0. T is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (0. T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . f) + (- (0. T)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(L . f) - (0. T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

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

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

(0_ (n,T)) *' L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

((0_ (n,T)) *' L) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

K501(2,(Bags n)) is M29( Bags n)

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

g is Relation-like NAT -defined the carrier of T -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of T

Sum g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

dom g is finite Element of bool NAT

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

(decomp f) /. f9 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K501(2,(Bags n))

g /. f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

g9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

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

(0_ (n,T)) . g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

((0_ (n,T)) . g9) * (L . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

0. T is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(0. T) * (L . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(0_ (n,T)) . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable V102() associative commutative 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 carrier of T is non zero non trivial set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

Polynom-Ring (n,T) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V102() associative commutative 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 carrier of (Polynom-Ring (n,T)) is non zero set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

- L is non zero Relation-like Bags n -defined Bags n -defined the carrier of T -valued Function-like total total V46( Bags n, the carrier of T) V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

- P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

f9 + P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

(- L) + L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

0. (Polynom-Ring (n,T)) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

the ZeroF of (Polynom-Ring (n,T)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable V102() associative commutative 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 carrier of T is non zero non trivial set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

L *' P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

- (L *' P) is non zero Relation-like Bags n -defined Bags n -defined the carrier of T -valued Function-like total total V46( Bags n, the carrier of T) V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

- L is non zero Relation-like Bags n -defined Bags n -defined the carrier of T -valued Function-like total total V46( Bags n, the carrier of T) V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

(- L) *' P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

- P is non zero Relation-like Bags n -defined Bags n -defined the carrier of T -valued Function-like total total V46( Bags n, the carrier of T) V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

L *' (- P) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

Polynom-Ring (n,T) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V102() associative commutative 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 carrier of (Polynom-Ring (n,T)) is non zero set

f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

g is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

f9 * g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

- f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

(- f9) * g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

- g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

f9 * (- g9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

- (f9 * g9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

0. T is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like finite-Support Element of bool [:(Bags n), the carrier of T:]

term P is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

P . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

Support P is functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

Support P is functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

{(term P)} is non zero trivial functional finite 1 -element set

Support P is functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

{(term P)} is non zero trivial functional finite 1 -element set

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable right_add-cancelable 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 T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) finite-Support Element of bool [:(Bags n), the carrier of T:]

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like finite-Support Element of bool [:(Bags n), the carrier of T:]

P *' L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

term P is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

P . (term P) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(term P) + f is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(P *' L) . ((term P) + f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(P . (term P)) * (L . f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

decomp ((term P) + f) is non zero Relation-like NAT -defined K501(2,(Bags n)) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V135() FinSequence-yielding finite-support FinSequence of K501(2,(Bags n))

K501(2,(Bags n)) is M29( Bags n)

len (decomp ((term P) + f)) is non zero epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real positive non negative complex Element of NAT

g9 is Relation-like NAT -defined the carrier of T -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of T

Sum g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

dom g9 is finite Element of bool NAT

dom (decomp ((term P) + f)) is non zero finite Element of bool NAT

<*(term P),f*> is non zero Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like finite-support set

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

(decomp ((term P) + f)) /. f9 is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K501(2,(Bags n))

Seg (len g9) is finite len g9 -element Element of bool NAT

g9 /. f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

g9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

R is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

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

P . g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(P . g9) * (L . R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

<*(term P),f*> . 2 is set

0. T is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

g9 /. x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(decomp ((term P) + f)) /. x is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of K501(2,(Bags n))

x is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

q is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

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

P . x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(P . x) * (L . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

divisors ((term P) + f) is non zero Relation-like NAT -defined Bags n -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags n

(divisors ((term P) + f)) /. x is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

((term P) + f) -' x is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

<*x,(((term P) + f) -' x)*> is non zero Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like finite-support set

<*x,(((term P) + f) -' x)*> . 2 is set

<*x,q*> . 2 is set

(decomp ((term P) + f)) . x is FinSequence-like set

(decomp ((term P) + f)) . f9 is FinSequence-like set

<*g9,R*> . 1 is set

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

0. T is zero left_add-cancelable Element of the carrier of T

the ZeroF of T is left_add-cancelable Element of the carrier of T

0_ (n,T) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) monomial-like Constant finite-Support Element of bool [:(Bags n), the carrier of T:]

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

(0. T) * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f is set

dom ((0. T) * L) is non zero functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

g is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

((0. T) * L) . g is left_add-cancelable Element of the carrier of T

L . g is left_add-cancelable Element of the carrier of T

(0. T) * (L . g) is left_add-cancelable Element of the carrier of T

((0. T) * L) . f is set

(0_ (n,T)) . f is set

dom (0_ (n,T)) is non zero functional Element of bool (Bags n)

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable right_add-cancelable 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 T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

- L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

- (P * L) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

- P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- P) * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P * (- L) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

g is set

dom (- (P * L)) is non zero functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(- (P * L)) . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(P * L) . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- ((P * L) . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P * (L . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (P * (L . f9)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- P) * (L . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

((- P) * L) . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (P * L)) . g is set

((- P) * L) . g is set

dom ((- P) * L) is non zero functional Element of bool (Bags n)

g is set

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(- (P * L)) . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(P * L) . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- ((P * L) . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P * (L . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (P * (L . f9)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (L . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P * (- (L . f9)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- L) . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

P * ((- L) . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(P * (- L)) . f9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- (P * L)) . g is set

(P * (- L)) . g is set

dom (P * (- L)) is non zero functional Element of bool (Bags n)

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left-distributive doubleLoopStr

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P is Element of the carrier of T

P * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f is Element of the carrier of T

f * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

(P * L) + (f * L) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P + f is Element of the carrier of T

(P + f) * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

g9 is set

dom ((P * L) + (f * L)) is non zero functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

((P * L) + (f * L)) . f9 is Element of the carrier of T

(P * L) . f9 is Element of the carrier of T

(f * L) . f9 is Element of the carrier of T

((P * L) . f9) + ((f * L) . f9) is Element of the carrier of T

L . f9 is Element of the carrier of T

P * (L . f9) is Element of the carrier of T

(P * (L . f9)) + ((f * L) . f9) is Element of the carrier of T

f * (L . f9) is Element of the carrier of T

(P * (L . f9)) + (f * (L . f9)) is Element of the carrier of T

(P + f) * (L . f9) is Element of the carrier of T

((P + f) * L) . f9 is Element of the carrier of T

((P * L) + (f * L)) . g9 is set

((P + f) * L) . g9 is set

dom ((P + f) * L) is non zero functional Element of bool (Bags n)

n is set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty associative multLoopStr_0

the carrier of T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P is Element of the carrier of T

f is Element of the carrier of T

P * f is Element of the carrier of T

(P * f) * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f * L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P * (f * L) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

g9 is set

dom ((P * f) * L) is non zero functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

f9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

((P * f) * L) . f9 is Element of the carrier of T

L . f9 is Element of the carrier of T

(P * f) * (L . f9) is Element of the carrier of T

f * (L . f9) is Element of the carrier of T

P * (f * (L . f9)) is Element of the carrier of T

(f * L) . f9 is Element of the carrier of T

P * ((f * L) . f9) is Element of the carrier of T

(P * (f * L)) . f9 is Element of the carrier of T

((P * f) * L) . g9 is set

(P * (f * L)) . g9 is set

dom (P * (f * L)) is non zero functional Element of bool (Bags n)

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non zero set

bool (Bags n) is cup-closed diff-closed preBoolean set

T is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V102() associative commutative 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 T is non zero set

[:(Bags n), the carrier of T:] is Relation-like set

bool [:(Bags n), the carrier of T:] is cup-closed diff-closed preBoolean set

L is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

L *' P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

f * (L *' P) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f * P is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

L *' (f * P) is non zero Relation-like Bags n -defined the carrier of T -valued Function-like total V46( Bags n, the carrier of T) Element of bool [:(Bags n), the carrier of T:]

f9 is set

dom (f * (L *' P)) is non zero functional Element of bool (Bags n)

bool (Bags n) is cup-closed diff-closed preBoolean set

g9 is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support set

(L *' (f * P)) . g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

K501(2,(Bags n)) is M29( Bags n)

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

R is Relation-like NAT -defined the carrier of T -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of T

Sum R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

dom R is finite Element of bool NAT

(L *' P) . g9 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

x is Relation-like NAT -defined the carrier of T