:: POLYNOM7 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V34() V35() Element of bool REAL

bool REAL is non empty set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V34() V35() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

[:2,2:] is non empty finite set

[:[:2,2:],2:] is non empty finite set

bool [:[:2,2:],2:] is non empty finite V33() set

{} is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite V33() V34() V36( {} ) ext-real V174() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

{{},1} is non empty finite V33() set

COMPLEX is set

RAT is set

INT is set

[:NAT,NAT:] is non empty non trivial non finite set

bool [:NAT,NAT:] is non empty non trivial non finite set

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

Seg 1 is Element of bool NAT

{1} is non empty trivial finite V33() V36(1) set

Seg 2 is Element of bool NAT

{1,2} is non empty finite V33() set

0 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite V33() V34() V36( {} ) ext-real V174() Element of NAT

Bags {} is functional non empty Element of bool (Bags {})

Bags {} is non empty set

bool (Bags {}) is non empty set

{{}} is non empty trivial finite V33() V36(1) set

the non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital 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 Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty non trivial ZeroStr

the carrier of L is non empty non trivial set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

NonZero L is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

[#] L is non empty non proper Element of bool the carrier of L

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

{(0. L)} is non empty trivial finite V36(1) set

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

the Element of NonZero L is Element of NonZero L

{(0. L)} is non empty trivial finite V36(1) Element of bool the carrier of L

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

a is Element of the carrier of L

(0_ (n,L)) +* ((EmptyBag n),a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

[:(Bags n),{(0. L)}:] is non empty set

dom (0_ (n,L)) is functional Element of bool (Bags n)

bool (Bags n) is non empty set

r . (EmptyBag n) is Element of the carrier of L

n is epsilon-transitive epsilon-connected ordinal set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty non trivial ZeroStr

the carrier of L is non empty non trivial set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

NonZero L is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

[#] L is non empty non proper Element of bool the carrier of L

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

{(0. L)} is non empty trivial finite V36(1) set

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

the Element of NonZero L is Element of NonZero L

{(0. L)} is non empty trivial finite V36(1) Element of bool the carrier of L

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support Element of bool [:(Bags n), the carrier of L:]

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

a is Element of the carrier of L

(0_ (n,L)) +* ((EmptyBag n),a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

q is set

r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

Support r is functional Element of bool (Bags n)

bool (Bags n) is non empty set

r . q is set

(0_ (n,L)) . q is set

{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)

(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

[:(Bags n),{(0. L)}:] is non empty set

dom (0_ (n,L)) is functional Element of bool (Bags n)

r . (EmptyBag n) is Element of the carrier of L

q is set

q is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support Element of bool [:(Bags n), the carrier of L:]

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

Support p is functional Element of bool (Bags n)

bool (Bags n) is non empty set

a is set

x is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

p . x is Element of the carrier of L

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

p . a is set

(0_ (n,L)) . a is set

dom p is functional Element of bool (Bags n)

dom (0_ (n,L)) is functional Element of bool (Bags n)

the Relation-like n -defined Function-like Element of Support p is Relation-like n -defined Function-like Element of Support p

x is Relation-like n -defined Function-like total V208() finite-support set

p . x is Element of the carrier of L

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

{(0. L)} is non empty trivial finite V36(1) set

a is set

{(0. L)} is non empty trivial finite V36(1) Element of bool the carrier of L

bool the carrier of L is non empty set

a is set

a is set

{a} is non empty trivial finite V36(1) set

a is Element of the carrier of L

a is Element of the carrier of L

(Bags n) --> a is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{a} is non empty trivial finite V36(1) set

[:(Bags n),{a}:] is non empty set

y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

q is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

q . (EmptyBag n) is Element of the carrier of L

Support q is functional Element of bool (Bags n)

bool (Bags n) is non empty set

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

Support p is functional Element of bool (Bags n)

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

Support p is functional Element of bool (Bags n)

the Relation-like n -defined Function-like Element of Support p is Relation-like n -defined Function-like Element of Support p

y is set

{y} is non empty trivial finite V36(1) set

y is set

{y} is non empty trivial finite V36(1) set

x is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

p . x is Element of the carrier of L

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

Support p is functional Element of bool (Bags n)

x is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

Support x is functional Element of bool (Bags n)

n is set

n is non empty set

the Element of n is Element of n

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

Bags n is non empty set

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

bool (Bags n) is non empty set

(EmptyBag n) +* ( the Element of n,1) is Relation-like n -defined Function-like total V208() finite-support set

dom (EmptyBag n) is Element of bool n

bool n is non empty set

((EmptyBag n) +* ( the Element of n,1)) . the Element of n is set

the Element of n .--> 1 is Relation-like n -defined { the Element of n} -defined NAT -valued Function-like one-to-one finite finite-support set

{ the Element of n} is non empty trivial finite V36(1) set

{ the Element of n} --> 1 is Relation-like non-empty { the Element of n} -defined NAT -valued {1} -valued Function-like constant non empty total V18({ the Element of n},{1}) finite finite-support Element of bool [:{ the Element of n},{1}:]

[:{ the Element of n},{1}:] is non empty finite set

bool [:{ the Element of n},{1}:] is non empty finite V33() set

(EmptyBag n) +* ( the Element of n .--> 1) is Relation-like Function-like set

((EmptyBag n) +* ( the Element of n .--> 1)) . the Element of n is set

dom ( the Element of n .--> 1) is finite Element of bool n

{ the Element of n} is non empty trivial finite V36(1) Element of bool n

support ((EmptyBag n) +* ( the Element of n,1)) is finite set

a is set

((EmptyBag n) +* ( the Element of n,1)) . a is set

((EmptyBag n) +* ( the Element of n .--> 1)) . a is set

(EmptyBag n) . a is set

( the Element of n .--> 1) . the Element of n is set

a is set

n is non empty set

L is Relation-like n -defined Function-like total V208() finite-support set

support L is finite set

p is Element of n

{p} is non empty trivial finite V36(1) Element of bool n

bool n is non empty set

L . p is set

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

Bags n is non empty set

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

bool (Bags n) is non empty set

(EmptyBag n) . p is set

EmptyBag {} is Relation-like {} -defined Function-like total V208() finite-support Element of Bags {}

L is Relation-like {} -defined Function-like total V208() finite-support set

p is Relation-like {} -defined Function-like total V208() finite-support set

{(EmptyBag {})} is functional non empty trivial finite V36(1) Element of bool (Bags {})

bool (Bags {}) is non empty set

L is non empty doubleLoopStr

the carrier of L is non empty set

[:(Bags {}), the carrier of L:] is non empty set

bool [:(Bags {}), the carrier of L:] is non empty set

p is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

a is Relation-like {} -defined Function-like total V208() finite-support set

[:{{}}, the carrier of L:] is non empty set

bool [:{{}}, the carrier of L:] is non empty set

a is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

x is Relation-like {{}} -defined the carrier of L -valued Function-like V18({{}}, the carrier of L) finite finite-support Element of bool [:{{}}, the carrier of L:]

x /. {} is Element of the carrier of L

dom x is trivial finite V33() Element of bool {{}}

bool {{}} is non empty finite V33() set

{(x /. {})} is non empty trivial finite V36(1) Element of bool the carrier of L

bool the carrier of L is non empty set

[:{(EmptyBag {})},{(x /. {})}:] is non empty finite set

z is set

r is set

q is set

[r,q] is set

r is Relation-like {} -defined Function-like total V208() finite-support set

x . {} is set

{(EmptyBag {})} --> (x /. {}) is Relation-like {(EmptyBag {})} -defined the carrier of L -valued Function-like constant non empty total V18({(EmptyBag {})}, the carrier of L) finite finite-support Element of bool [:{(EmptyBag {})}, the carrier of L:]

[:{(EmptyBag {})}, the carrier of L:] is non empty set

bool [:{(EmptyBag {})}, the carrier of L:] is non empty set

{(x /. {})} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{(x /. {})}:] is non empty finite set

z is set

r is set

q is set

[r,q] is set

x . {} is set

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty non trivial set

[:(Bags {}), the carrier of L:] is non empty set

bool [:(Bags {}), the carrier of L:] is non empty set

[:{}, the carrier of L:] is set

bool [:{}, the carrier of L:] is non empty set

p is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

p . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

a is Relation-like {} -defined the carrier of L -valued Function-like one-to-one constant functional empty V18( {} , the carrier of L) epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite finite-yielding V33() V34() V36( {} ) Function-yielding V159() ext-real V174() FinSequence-yielding finite-support Element of bool [:{}, the carrier of L:]

eval (p,a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

x is Relation-like {} -defined Function-like total V208() finite-support set

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

{(EmptyBag {})} --> x is Relation-like {(EmptyBag {})} -defined the carrier of L -valued Function-like constant non empty total V18({(EmptyBag {})}, the carrier of L) finite finite-support Element of bool [:{(EmptyBag {})}, the carrier of L:]

[:{(EmptyBag {})}, the carrier of L:] is non empty set

bool [:{(EmptyBag {})}, the carrier of L:] is non empty set

{x} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{x}:] is non empty finite set

dom p is functional Element of bool (Bags {})

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

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

Support p is functional finite Element of bool (Bags {})

the Relation-like {} -defined Function-like Element of Support p is Relation-like {} -defined Function-like Element of Support p

z is Relation-like {} -defined Function-like total V208() finite-support Element of Bags {}

p . z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

BagOrder {} is Relation-like Bags {} -defined Bags {} -valued total being_linear-order V197() V200() V204() Element of bool [:(Bags {}),(Bags {}):]

[:(Bags {}),(Bags {}):] is non empty set

bool [:(Bags {}),(Bags {}):] is non empty set

SgmX ((BagOrder {}),(Support p)) is Relation-like NAT -defined Bags {} -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags {}

len (SgmX ((BagOrder {}),(Support p))) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

p * (SgmX ((BagOrder {}),(Support p))) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]

[:NAT, the carrier of L:] is non empty non trivial non finite set

bool [:NAT, the carrier of L:] is non empty non trivial non finite set

z is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len z is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

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

y is Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite V33() V34() V36( {} ) ext-real V174() Element of bool (Bags {})

SgmX ((BagOrder {}),y) is Relation-like NAT -defined Bags {} -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags {}

<*> the carrier of L is Relation-like NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() finite finite-yielding V33() V34() V36( {} ) FinSequence-like Function-yielding V159() ext-real V174() FinSequence-yielding finite-support M36( the carrier of L,K468( the carrier of L))

K468( the carrier of L) is M35( the carrier of L)

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

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

Support p is functional finite Element of bool (Bags {})

y is functional finite Element of bool (Bags {})

BagOrder {} is Relation-like Bags {} -defined Bags {} -valued total being_linear-order V197() V200() V204() Element of bool [:(Bags {}),(Bags {}):]

[:(Bags {}),(Bags {}):] is non empty set

bool [:(Bags {}),(Bags {}):] is non empty set

SgmX ((BagOrder {}),y) is Relation-like NAT -defined Bags {} -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags {}

r is set

q is Relation-like {} -defined Function-like total V208() finite-support Element of Bags {}

r is set

rng (SgmX ((BagOrder {}),y)) is set

dom (SgmX ((BagOrder {}),y)) is Element of bool NAT

(SgmX ((BagOrder {}),y)) . 1 is Relation-like Function-like set

p * (SgmX ((BagOrder {}),y)) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]

[:NAT, the carrier of L:] is non empty non trivial non finite set

bool [:NAT, the carrier of L:] is non empty non trivial non finite set

dom (p * (SgmX ((BagOrder {}),y))) is Element of bool NAT

(p * (SgmX ((BagOrder {}),y))) /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

(p * (SgmX ((BagOrder {}),y))) . 1 is set

p . ((SgmX ((BagOrder {}),y)) . 1) is set

{1} is non empty trivial finite V33() V36(1) Element of bool NAT

r is set

q is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

(SgmX ((BagOrder {}),y)) /. q is Relation-like {} -defined Function-like total V208() finite-support Element of Bags {}

(SgmX ((BagOrder {}),y)) . q is Relation-like Function-like set

r is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() set

Seg r is Element of bool NAT

{ b

q is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

(SgmX ((BagOrder {}),y)) /. 1 is Relation-like {} -defined Function-like total V208() finite-support Element of Bags {}

r is set

len (SgmX ((BagOrder {}),y)) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

r is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len r is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

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

dom r is Element of bool NAT

Seg (len r) is Element of bool NAT

r . 1 is set

r /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

(SgmX ((BagOrder {}),y)) /. 1 is Relation-like {} -defined Function-like total V208() finite-support Element of Bags {}

((SgmX ((BagOrder {}),y)) /. 1) @ is Relation-like {} -defined Function-like total V208() finite-support set

eval ((((SgmX ((BagOrder {}),y)) /. 1) @),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

((p * (SgmX ((BagOrder {}),y))) /. 1) * (eval ((((SgmX ((BagOrder {}),y)) /. 1) @),a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

eval ((EmptyBag {}),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

((p * (SgmX ((BagOrder {}),y))) /. 1) * (eval ((EmptyBag {}),a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

1. L is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

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

((p * (SgmX ((BagOrder {}),y))) /. 1) * (1. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

<*x*> is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like M36( the carrier of L,K468( the carrier of L))

K468( the carrier of L) is M35( the carrier of L)

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

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

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

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

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

Polynom-Ring ({},L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive right_unital well-unital left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty non trivial set

[:(Bags {}), the carrier of L:] is non empty set

bool [:(Bags {}), the carrier of L:] is non empty set

0_ ({},L) is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

dom (0_ ({},L)) is functional Element of bool (Bags {})

{(EmptyBag {})} is functional non empty trivial finite V36(1) set

1_ L is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

1. L is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

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

(EmptyBag {}) .--> (1_ L) is Relation-like Bags {} -defined {(EmptyBag {})} -defined the carrier of L -valued Function-like one-to-one finite finite-support set

{(EmptyBag {})} --> (1_ L) is Relation-like {(EmptyBag {})} -defined the carrier of L -valued {(1_ L)} -valued Function-like constant non empty total V18({(EmptyBag {})},{(1_ L)}) finite finite-support Element of bool [:{(EmptyBag {})},{(1_ L)}:]

{(1_ L)} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{(1_ L)}:] is non empty finite set

bool [:{(EmptyBag {})},{(1_ L)}:] is non empty finite V33() set

dom ((EmptyBag {}) .--> (1_ L)) is functional trivial finite Element of bool {(EmptyBag {})}

bool {(EmptyBag {})} is non empty finite V33() set

a is Relation-like {} -defined Function-like total V208() finite-support set

the carrier of (Polynom-Ring ({},L)) is non empty set

x is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

y is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

y . {} is set

dom y is functional Element of bool (Bags {})

rng y is set

[: the carrier of (Polynom-Ring ({},L)), the carrier of L:] is non empty set

bool [: the carrier of (Polynom-Ring ({},L)), the carrier of L:] is non empty set

x is Relation-like the carrier of (Polynom-Ring ({},L)) -defined the carrier of L -valued Function-like V18( the carrier of (Polynom-Ring ({},L)), the carrier of L) Element of bool [: the carrier of (Polynom-Ring ({},L)), the carrier of L:]

dom x is Element of bool the carrier of (Polynom-Ring ({},L))

bool the carrier of (Polynom-Ring ({},L)) is non empty set

1_ (Polynom-Ring ({},L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

1. (Polynom-Ring ({},L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

the OneF of (Polynom-Ring ({},L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

y is Relation-like the carrier of (Polynom-Ring ({},L)) -defined the carrier of L -valued Function-like V18( the carrier of (Polynom-Ring ({},L)), the carrier of L) Element of bool [: the carrier of (Polynom-Ring ({},L)), the carrier of L:]

y . (1. (Polynom-Ring ({},L))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

z is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

z . {} is set

1_ ({},L) is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

(0_ ({},L)) +* ((EmptyBag {}),(1_ L)) is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

r * q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

y . (r * q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

y . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

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

(y . r) * (y . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

r is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

r . {} is set

q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

q . {} is set

r *' q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

(r *' q) . {} is set

a is Relation-like {} -defined Function-like total V208() finite-support set

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

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

(r . a) * (q . a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

decomp (EmptyBag {}) is Relation-like NAT -defined K469(2,(Bags {})) -valued Function-like one-to-one non empty FinSequence-like Function-yielding V159() FinSequence-yielding FinSequence of K469(2,(Bags {}))

K469(2,(Bags {})) is M35( Bags {})

[:NAT,(Bags {}):] is non empty non trivial non finite set

bool [:NAT,(Bags {}):] is non empty non trivial non finite set

<*(EmptyBag {}),(EmptyBag {})*> is Relation-like NAT -defined Bags {} -valued Function-like FinSequence-like Function-yielding V159() M36( Bags {},K468((Bags {})))

K468((Bags {})) is M35( Bags {})

<*<*(EmptyBag {}),(EmptyBag {})*>*> is Relation-like NAT -defined bool [:NAT,(Bags {}):] -valued Function-like FinSequence-like Function-yielding V159() FinSequence-yielding M36( bool [:NAT,(Bags {}):],K468((bool [:NAT,(Bags {}):])))

K468((bool [:NAT,(Bags {}):])) is M35( bool [:NAT,(Bags {}):])

len (decomp (EmptyBag {})) is non empty epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

(r *' q) . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

k is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

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

len k is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT

dom k is Element of bool NAT

(decomp (EmptyBag {})) /. 1 is Relation-like Bags {} -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags {}))

k /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

c is Relation-like {} -defined Function-like total V208() finite-support set

c is Relation-like {} -defined Function-like total V208() finite-support set

<*c,c*> is set

r . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

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

(r . c) * (q . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

k . 1 is set

(r . a) * (q . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

<*((r . a) * (q . a))*> is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like M36( the carrier of L,K468( the carrier of L))

K468( the carrier of L) is M35( the carrier of L)

i is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

i . {} is set

r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

r + q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

y . (r + q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

y . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

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

(y . r) + (y . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

r is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

r . {} is set

q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

q . {} is set

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

{(EmptyBag {})} --> i is Relation-like {(EmptyBag {})} -defined the carrier of L -valued Function-like constant non empty total V18({(EmptyBag {})}, the carrier of L) finite finite-support Element of bool [:{(EmptyBag {})}, the carrier of L:]

[:{(EmptyBag {})}, the carrier of L:] is non empty set

bool [:{(EmptyBag {})}, the carrier of L:] is non empty set

{i} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{i}:] is non empty finite set

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

{(EmptyBag {})} --> k is Relation-like {(EmptyBag {})} -defined the carrier of L -valued Function-like constant non empty total V18({(EmptyBag {})}, the carrier of L) finite finite-support Element of bool [:{(EmptyBag {})}, the carrier of L:]

{k} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{k}:] is non empty finite set

r + q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

(r + q) . {} is set

a is Relation-like {} -defined Function-like total V208() finite-support set

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

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

(r . a) + (q . a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

i + k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

c . {} is set

a is Relation-like {} -defined Function-like total V208() finite-support set

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

z . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

(0_ ({},L)) +* ((EmptyBag {}) .--> (1_ L)) is Relation-like Function-like set

((0_ ({},L)) +* ((EmptyBag {}) .--> (1_ L))) . (EmptyBag {}) is set

((EmptyBag {}) .--> (1_ L)) . (EmptyBag {}) is set

rng y is set

r is set

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

(EmptyBag {}) .--> q is Relation-like Bags {} -defined {(EmptyBag {})} -defined the carrier of L -valued Function-like one-to-one finite finite-support set

{(EmptyBag {})} --> q is Relation-like {(EmptyBag {})} -defined the carrier of L -valued {q} -valued Function-like constant non empty total V18({(EmptyBag {})},{q}) finite finite-support Element of bool [:{(EmptyBag {})},{q}:]

{q} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{q}:] is non empty finite set

bool [:{(EmptyBag {})},{q}:] is non empty finite V33() set

q is Relation-like Function-like set

dom q is set

rng q is set

{q} is non empty trivial finite V36(1) Element of bool the carrier of L

bool the carrier of L is non empty set

i is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

k is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

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

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

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

Support c is functional Element of bool (Bags {})

the Relation-like {} -defined Function-like Element of Support c is Relation-like {} -defined Function-like Element of Support c

c . the Relation-like {} -defined Function-like Element of Support c is set

c . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

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

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

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

Support c is functional Element of bool (Bags {})

c is set

b2 is Relation-like {} -defined Function-like total V208() finite-support Element of Bags {}

c . b2 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

c . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

c is set

b2 is Relation-like {} -defined Function-like total V208() finite-support set

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

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

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

Support c is functional Element of bool (Bags {})

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

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

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(Bags {}), the carrier of L:]

Support c is functional Element of bool (Bags {})

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

b2 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

y . b2 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

q . {} is set

c . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

r is set

dom y is Element of bool the carrier of (Polynom-Ring ({},L))

r is set

q is set

y . r is set

y . q is set

r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

y . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

i is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

i . {} is set

q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))

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

k is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(Bags {}), the carrier of L:]

k . {} is set

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

{(EmptyBag {})} --> c is Relation-like {(EmptyBag {})} -defined the carrier of L -valued Function-like constant non empty total V18({(EmptyBag {})}, the carrier of L) finite finite-support Element of bool [:{(EmptyBag {})}, the carrier of L:]

[:{(EmptyBag {})}, the carrier of L:] is non empty set

bool [:{(EmptyBag {})}, the carrier of L:] is non empty set

{c} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{c}:] is non empty finite set

k . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

i . (EmptyBag {}) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

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

{(EmptyBag {})} --> c is Relation-like {(EmptyBag {})} -defined the carrier of L -valued Function-like constant non empty total V18({(EmptyBag {})}, the carrier of L) finite finite-support Element of bool [:{(EmptyBag {})}, the carrier of L:]

{c} is non empty trivial finite V36(1) set

[:{(EmptyBag {})},{c}:] is non empty finite set

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

a is Relation-like n -defined Function-like total V208() finite-support set

(0_ (n,L)) . a is Element of the carrier of L

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

a is Relation-like n -defined Function-like total V208() finite-support set

p . a is Element of the carrier of L

Support p is functional Element of bool (Bags n)

bool (Bags n) is non empty set

x is functional non empty Element of bool (Bags n)

the Relation-like n -defined Function-like total V208() finite-support Element of x is Relation-like n -defined Function-like total V208() finite-support Element of x

p . the Relation-like n -defined Function-like total V208() finite-support Element of x is Element of the carrier of L

p . a is Element of the carrier of L

x is set

Support p is functional Element of bool (Bags n)

bool (Bags n) is non empty set

y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

p . y is Element of the carrier of L

{a} is functional non empty trivial finite V36(1) set

x is set

y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

p . a is Element of the carrier of L

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

Support p is functional Element of bool (Bags n)

bool (Bags n) is non empty set

a is Relation-like n -defined Function-like total V208() finite-support set

{a} is functional non empty trivial finite V36(1) set

a is Relation-like n -defined Function-like total V208() finite-support set

{a} is functional non empty trivial finite V36(1) set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

x is Relation-like n -defined Function-like total V208() finite-support set

p . x is Element of the carrier of L

y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

a is Relation-like n -defined Function-like total V208() finite-support set

p . a is Element of the carrier of L

{a} is functional non empty trivial finite V36(1) set

x is set

y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

p . y is Element of the carrier of L

x is set

p . x is set

y is Relation-like n -defined Function-like total V208() finite-support set

p . a is Element of the carrier of L

x is functional non empty Element of bool (Bags n)

the Relation-like n -defined Function-like total V208() finite-support Element of x is Relation-like n -defined Function-like total V208() finite-support Element of x

p . the Relation-like n -defined Function-like total V208() finite-support Element of x is Element of the carrier of L

p . a is Element of the carrier of L

p . a is Element of the carrier of L

x is Relation-like n -defined Function-like total V208() finite-support set

{x} is functional non empty trivial finite V36(1) set

the Relation-like n -defined Function-like total V208() finite-support set is Relation-like n -defined Function-like total V208() finite-support set

x is Relation-like n -defined Function-like total V208() finite-support set

p . x is Element of the carrier of L

y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

a is Relation-like n -defined Function-like total V208() finite-support set

{a} is functional non empty trivial finite V36(1) set

x is Relation-like n -defined Function-like total V208() finite-support set

{x} is functional non empty trivial finite V36(1) set

L is non empty ZeroStr

the carrier of L is non empty set

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

a is Relation-like n -defined Function-like total V208() finite-support set

p is Element of the carrier of L

(0_ (n,L)) +* (a,p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{a} is functional non empty trivial finite V36(1) set

a .--> p is Relation-like {a} -defined the carrier of L -valued Function-like one-to-one finite finite-support set

{a} --> p is Relation-like {a} -defined the carrier of L -valued {p} -valued Function-like constant non empty total V18({a},{p}) finite finite-support Element of bool [:{a},{p}:]

{p} is non empty trivial finite V36(1) set

[:{a},{p}:] is non empty finite set

bool [:{a},{p}:] is non empty finite V33() set

dom (a .--> p) is functional trivial finite Element of bool {a}

bool {a} is non empty finite V33() set

y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

dom (0_ (n,L)) is functional Element of bool (Bags n)

bool (Bags n) is non empty set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{(0. L)} is non empty trivial finite V36(1) set

[:(Bags n),{(0. L)}:] is non empty set

dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)

r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(0_ (n,L)) +* (a .--> p) is Relation-like Function-like set

r . a is Element of the carrier of L

((0_ (n,L)) +* (a .--> p)) . a is set

(a .--> p) . a is set

Support r is functional Element of bool (Bags n)

q is set

r is Relation-like n -defined Function-like total V208() finite-support set

r . r is Element of the carrier of L

(0_ (n,L)) . r is Element of the carrier of L

q is set

Support r is functional Element of bool (Bags n)

q is functional non empty Element of bool (Bags n)

the Relation-like n -defined Function-like total V208() finite-support Element of q is Relation-like n -defined Function-like total V208() finite-support Element of q

r . the Relation-like n -defined Function-like total V208() finite-support Element of q is Element of the carrier of L

q is Relation-like n -defined Function-like total V208() finite-support set

r . q is Element of the carrier of L

(0_ (n,L)) . q is Element of the carrier of L

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

Support p is functional Element of bool (Bags n)

bool (Bags n) is non empty set

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

a is Relation-like n -defined Function-like total V208() finite-support set

p . a is Element of the carrier of L

p . a is Element of the carrier of L

x is functional non empty Element of bool (Bags n)

the Relation-like n -defined Function-like total V208() finite-support Element of x is Relation-like n -defined Function-like total V208() finite-support Element of x

p . the Relation-like n -defined Function-like total V208() finite-support Element of x is Element of the carrier of L

p . a is Element of the carrier of L

p . a is Element of the carrier of L

x is Relation-like n -defined Function-like total V208() finite-support set

p . x is Element of the carrier of L

y is Relation-like n -defined Function-like total V208() finite-support set

z is Relation-like n -defined Function-like total V208() finite-support set

p . z is Element of the carrier of L

r is Relation-like n -defined Function-like total V208() finite-support set

a is Relation-like n -defined Function-like total V208() finite-support set

p . a is Element of the carrier of L

x is Relation-like n -defined Function-like total V208() finite-support set

p . x is Element of the carrier of L

y is Relation-like n -defined Function-like total V208() finite-support set

z is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

z is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]

(n,L,p) is Relation-like n -defined Function-like total V208() finite-support set

p . (n,L,p) is Element of the carrier of L

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]

Support p is functional Element of bool (Bags n)

bool (Bags n) is non empty set

(n,L,p) is Relation-like n -defined Function-like total V208() finite-support set

{(n,L,p)} is functional non empty trivial finite V36(1) set

p . (n,L,p) is Element of the carrier of L

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

a is Relation-like n -defined Function-like total V208() finite-support set

{a} is functional non empty trivial finite V36(1) set

n is set

EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n

Bags n is non empty set

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

bool (Bags n) is non empty set

L is non empty ZeroStr

0. L is zero Element of the carrier of L

the carrier of L is non empty set

the ZeroF of L is Element of the carrier of L

p is Relation-like n -defined Function-like total V208() finite-support set

(n,L,(0. L),p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(0_ (n,L)) +* (p,(0. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(n,L,(n,L,(0. L),p)) is Element of the carrier of L

(n,L,(n,L,(0. L),p)) is Relation-like n -defined Function-like total V208() finite-support set

(n,L,(0. L),p) . (n,L,(n,L,(0. L),p)) is Element of the carrier of L

x is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

dom (0_ (n,L)) is functional Element of bool (Bags n)

bool (Bags n) is non empty set

(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{(0. L)} is non empty trivial finite V36(1) set

[:(Bags n),{(0. L)}:] is non empty set

dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)

z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

p .--> (0. L) is Relation-like {p} -defined the carrier of L -valued Function-like one-to-one finite finite-support set

{p} is functional non empty trivial finite V36(1) set

{p} --> (0. L) is Relation-like {p} -defined the carrier of L -valued {(0. L)} -valued Function-like constant non empty total V18({p},{(0. L)}) finite finite-support Element of bool [:{p},{(0. L)}:]

[:{p},{(0. L)}:] is non empty finite set

bool [:{p},{(0. L)}:] is non empty finite V33() set

(0_ (n,L)) +* (p .--> (0. L)) is Relation-like Function-like set

dom (p .--> (0. L)) is functional trivial finite Element of bool {p}

bool {p} is non empty finite V33() set

z . p is Element of the carrier of L

((0_ (n,L)) +* (p .--> (0. L))) . p is set

(p .--> (0. L)) . p is set

r is Relation-like n -defined Function-like total V208() finite-support set

z . r is Element of the carrier of L

r is Relation-like n -defined Function-like total V208() finite-support set

z . r is Element of the carrier of L

(0_ (n,L)) . r is Element of the carrier of L

r is Relation-like n -defined Function-like total V208() finite-support set

z . r is Element of the carrier of L

r is Relation-like n -defined Function-like total V208() finite-support set

z . r is Element of the carrier of L

n is set

L is non empty ZeroStr

the carrier of L is non empty set

p is Element of the carrier of L

a is Relation-like n -defined Function-like total V208() finite-support set

(n,L,p,a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]

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

Bags n is non empty set

bool (Bags n) is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(0_ (n,L)) +* (a,p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(n,L,(n,L,p,a)) is Element of the carrier of L

(n,L,(n,L,p,a)) is Relation-like n -defined Function-like total V208() finite-support set

(n,L,p,a) . (n,L,(n,L,p,a)) is Element of the carrier of L

y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{a} is functional non empty trivial finite V36(1) set

a .--> p is Relation-like {a} -defined the carrier of L -valued Function-like one-to-one finite finite-support set

{a} --> p is Relation-like {a} -defined the carrier of L -valued {p} -valued Function-like constant non empty total V18({a},{p}) finite finite-support Element of bool [:{a},{p}:]

{p} is non empty trivial finite V36(1) set

[:{a},{p}:] is non empty finite set

bool [:{a},{p}:] is non empty finite V33() set

dom (a .--> p) is functional trivial finite Element of bool {a}

bool {a} is non empty finite V33() set

dom (0_ (n,L)) is functional Element of bool (Bags n)

bool (Bags n) is non empty set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{(0. L)} is non empty trivial finite V36(1) set

[:(Bags n),{(0. L)}:] is non empty set

dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)

r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

r . a is Element of the carrier of L

(0_ (n,L)) +* (a .--> p) is Relation-like Function-like set

((0_ (n,L)) +* (a .--> p)) . a is set

(a .--> p) . a is set

n is set

L is non empty non trivial ZeroStr

the carrier of L is non empty non trivial set

p is non zero Element of the carrier of L

a is Relation-like n -defined Function-like total V208() finite-support set

(n,L,p,a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]

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

Bags n is non empty set

bool (Bags n) is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(0_ (n,L)) +* (a,p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

(n,L,(n,L,p,a)) is Relation-like n -defined Function-like total V208() finite-support set

y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{a} is functional non empty trivial finite V36(1) set

a .--> p is Relation-like {a} -defined the carrier of L -valued Function-like one-to-one finite finite-support set

{a} --> p is Relation-like {a} -defined the carrier of L -valued {p} -valued Function-like constant non empty total V18({a},{p}) finite finite-support Element of bool [:{a},{p}:]

{p} is non empty trivial finite V36(1) set

[:{a},{p}:] is non empty finite set

bool [:{a},{p}:] is non empty finite V33() set

dom (a .--> p) is functional trivial finite Element of bool {a}

bool {a} is non empty finite V33() set

dom (0_ (n,L)) is functional Element of bool (Bags n)

bool (Bags n) is non empty set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{(0. L)} is non empty trivial finite V36(1) set

[:(Bags n),{(0. L)}:] is non empty set

dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)

r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

r . a is Element of the carrier of L

(0_ (n,L)) +* (a .--> p) is Relation-like Function-like set

((0_ (n,L)) +* (a .--> p)) . a is set

(a .--> p) . a is set

n is set

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

Bags n is non empty set

bool (Bags n) is non empty set

L is non empty ZeroStr

the carrier of L is non empty set

[:(Bags n), the carrier of L:] is non empty set

bool [:(Bags n), the carrier of L:] is non empty set

p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(