:: 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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex Element of NAT : ( 1 <= b₁ & b₁ <= P + 1 ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() ext-real non negative complex Element of NAT : ( 1 <= b₁ & b₁ <= P ) } is set
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