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
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT : ( 1 <= b1 & b1 <= r ) } is set
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 [:(