:: POLYRED semantic presentation

REAL is set

RAT is set
INT is set

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

is non trivial Relation-like non finite set
is non trivial Relation-like non finite set

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

Bags n is non zero functional Element of bool (Bags n)
Bags n is non zero 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

[#] 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:]

n is set

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

T is Element of bool n

field L is set

Bags n is non zero functional Element of bool (Bags n)
Bags n is non zero 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:]

f is functional finite Element of bool (Bags n)

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

{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

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

Support L is functional Element of bool (Bags n)
P is finite 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:]
g is functional finite Element of bool (Bags n)

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

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

L . f9 is Element of the carrier of T
L . g is Element of the carrier of T

the carrier of n is non zero set

(Sum L) + (T /. (len T)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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)

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

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

(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

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

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

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

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

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

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

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

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

rng (SgmX ((),f9)) is non zero finite set
dom (SgmX ((),f9)) is non zero finite Element of bool NAT
R is set
(SgmX ((),f9)) . R is Relation-like Function-like set
dom (decomp (g + f)) is non zero finite Element of bool NAT

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

(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

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

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

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

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)

((- L) + (- 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)) + ((- 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)) . 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

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

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

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

((- L) . f) + (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 . g) + ((- 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

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

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

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

(- (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
(L . f) + (- ((0_ (n,T)) . f)) 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

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

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

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

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

((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) * (L . f9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

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

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

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

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

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

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

the carrier of (Polynom-Ring (n,T)) is non zero set

(- 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))
- (f9 * g9) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,T))

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

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

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

Support P is functional 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:]
Support P is functional Element of bool (Bags n)

{(term P)} is non zero trivial functional finite 1 -element set
Support P is functional Element of bool (Bags n)

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

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

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

(P *' L) . ((term P) + 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

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

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

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

(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

(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)) /. x is Relation-like n -defined RAT -valued Function-like total V242() V243() V244() V245() finite-support Element of Bags n

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

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)

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

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

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

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

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)

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

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)

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

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

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

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

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

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