:: 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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT : ( 1 <= b₁ & b₁ <= 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 [:(Bags n), the carrier of L:]
(n,L,p) is Element of 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,L,(n,L,p),(n,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:]
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)) +* ((n,L,p),(n,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:]
dom p is functional Element of bool (Bags n)
bool (Bags n) is non empty set
dom (n,L,(n,L,p),(n,L,p)) is functional Element of bool (Bags n)
Support p is functional Element of bool (Bags n)
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
dom (0_ (n,L)) is functional 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:]
{(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)
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
{(EmptyBag n)} is functional non empty trivial finite V36(1) set
(EmptyBag n) .--> (0. L) is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} --> (0. L) is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {(0. L)} -valued Function-like constant non empty total V18({(EmptyBag n)},{(0. L)}) finite finite-support Element of bool [:{(EmptyBag n)},{(0. L)}:]
[:{(EmptyBag n)},{(0. L)}:] is non empty finite set
bool [:{(EmptyBag n)},{(0. L)}:] is non empty finite V33() set
dom ((EmptyBag n) .--> (0. L)) is functional trivial finite Element of bool {(EmptyBag n)}
bool {(EmptyBag n)} is non empty finite V33() set
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
(n,L,(n,L,p),(n,L,p)) . (EmptyBag n) is Element of the carrier of L
(0_ (n,L)) +* ((EmptyBag n) .--> (0. L)) is Relation-like Function-like set
((0_ (n,L)) +* ((EmptyBag n) .--> (0. L))) . (EmptyBag n) is set
((EmptyBag n) .--> (0. L)) . (EmptyBag n) is set
x is set
y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . y is Element of the carrier of L
y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . y is Element of the carrier of L
((0_ (n,L)) +* ((EmptyBag n) .--> (0. L))) . y is set
(0_ (n,L)) . y is Element of the carrier of L
y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . y is Element of the carrier of L
y is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . y is Element of the carrier of L
p . x is set
(n,L,(n,L,p),(n,L,p)) . x is set
Support p is functional Element of bool (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
a is Relation-like n -defined Function-like total V208() finite-support set
{a} is functional non empty trivial finite V36(1) set
p . a is Element of the carrier of L
a .--> (p . a) is Relation-like {a} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{a} --> (p . a) is Relation-like {a} -defined the carrier of L -valued {(p . a)} -valued Function-like constant non empty total V18({a},{(p . a)}) finite finite-support Element of bool [:{a},{(p . a)}:]
{(p . a)} is non empty trivial finite V36(1) set
[:{a},{(p . a)}:] is non empty finite set
bool [:{a},{(p . a)}:] is non empty finite V33() set
dom (a .--> (p . a)) 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)
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)
z is set
Support (n,L,(n,L,p),(n,L,p)) is functional Element of bool (Bags n)
r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . r is Element of the carrier of L
(0_ (n,L)) +* (a .--> (p . a)) is Relation-like Function-like set
((0_ (n,L)) +* (a .--> (p . a))) . r is set
(0_ (n,L)) . r is Element of the carrier of L
(n,L,(n,L,p),(n,L,p)) . a is Element of the carrier of L
((0_ (n,L)) +* (a .--> (p . a))) . a is set
(a .--> (p . a)) . a is set
z is set
z is set
r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . r is Element of the carrier of L
p . r is Element of the carrier of L
r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . r is Element of the carrier of L
(n,L,(n,L,p),(n,L,p)) . r is Element of the carrier of L
r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . r is Element of the carrier of L
p . r is Element of the carrier of L
r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,(n,L,p),(n,L,p)) . r is Element of the carrier of L
p . r is Element of the carrier of L
p . z is set
(n,L,(n,L,p),(n,L,p)) . z is set
Support p is functional Element of bool (Bags n)
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 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 n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
[:n, the carrier of L:] is set
bool [: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 left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p) is Relation-like n -defined Function-like total V208() finite-support set
p . (n,L,p) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval (p,a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval ((n,L,p),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p) * (eval ((n,L,p),a)) 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 n)
bool (Bags n) is non empty set
BagOrder n is Relation-like Bags n -defined Bags n -valued total being_linear-order V197() V200() V204() Element of bool [:(Bags n),(Bags n):]
[:(Bags n),(Bags n):] is non empty set
bool [:(Bags n),(Bags n):] is non empty set
SgmX ((BagOrder n),(Support p)) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
len (SgmX ((BagOrder n),(Support p))) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
p * (SgmX ((BagOrder n),(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
x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
len x is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
Sum x 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
y is Relation-like n -defined Function-like total V208() finite-support set
p . y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
{y} is functional non empty trivial finite V36(1) set
z is set
r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom p is functional Element of bool (Bags n)
z is functional finite Element of bool (Bags n)
SgmX ((BagOrder n),z) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
q is set
r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
rng (SgmX ((BagOrder n),z)) is set
dom (SgmX ((BagOrder n),z)) is Element of bool NAT
(SgmX ((BagOrder n),z)) . 1 is Relation-like Function-like set
p * (SgmX ((BagOrder n),z)) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
dom (p * (SgmX ((BagOrder n),z))) is Element of bool NAT
(p * (SgmX ((BagOrder n),z))) /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p * (SgmX ((BagOrder n),z))) . 1 is set
p . ((SgmX ((BagOrder n),z)) . 1) is set
{1} is non empty trivial finite V33() V36(1) Element of bool NAT
q is set
r is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(SgmX ((BagOrder n),z)) /. r is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(SgmX ((BagOrder n),z)) . r is Relation-like Function-like set
q is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() set
Seg q is Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT : ( 1 <= b₁ & b₁ <= q ) } is set
i is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(SgmX ((BagOrder n),z)) /. 1 is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
q is set
(SgmX ((BagOrder n),z)) /. 1 is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
len (SgmX ((BagOrder n),z)) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
dom x is Element of bool NAT
Seg (len x) is Element of bool NAT
x . 1 is set
x /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((SgmX ((BagOrder n),z)) /. 1) @ is Relation-like n -defined Function-like total V208() finite-support set
eval ((((SgmX ((BagOrder n),z)) /. 1) @),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((p * (SgmX ((BagOrder n),z))) /. 1) * (eval ((((SgmX ((BagOrder n),z)) /. 1) @),a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (y,a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((p * (SgmX ((BagOrder n),z))) /. 1) * (eval (y,a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p) * (eval (y,a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*((n,L,p) * (eval (y,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)
p . y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
z is functional non empty Element of bool (Bags n)
the Relation-like n -defined Function-like total V208() finite-support Element of z is Relation-like n -defined Function-like total V208() finite-support Element of z
p . the Relation-like n -defined Function-like total V208() finite-support Element of z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . (EmptyBag n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
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
rng (SgmX ((BagOrder n),(Support p))) is set
<*> 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)
p . y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
n is epsilon-transitive epsilon-connected ordinal 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
[:n, the carrier of L:] is set
bool [:n, the carrier of L:] is non empty set
p is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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) finite-Support 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:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((n,L,p,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (a,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p * (eval (a,x)) 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
(n,L,(n,L,p,a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval ((n,L,(n,L,p,a)),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,(n,L,p,a)) * (eval ((n,L,(n,L,p,a)),x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p * (eval ((n,L,(n,L,p,a)),x)) 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
z is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p,a) . z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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
(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)
(0_ (n,L)) +* (a .--> p) is Relation-like Function-like set
(a .--> p) . a is set
(0_ (n,L)) . z is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,(n,L,p,a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval ((n,L,(n,L,p,a)),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,(n,L,p,a)) * (eval ((n,L,(n,L,p,a)),x)) 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
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
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:]
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
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
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
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)
a is set
x is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
y is Relation-like n -defined Function-like total V208() finite-support set
p . y 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 set
the Relation-like n -defined Function-like Element of Support p is Relation-like n -defined Function-like Element of Support p
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
rng p 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
dom p is functional Element of bool (Bags n)
x is set
p . x is set
dom p is functional Element of bool (Bags n)
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 set
p . the Relation-like n -defined Function-like total V208() finite-support set 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
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
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
x is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
n is set
L is non empty ZeroStr
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 is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
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
p is Relation-like n -defined Function-like total V208() finite-support set
(0_ (n,L)) . p is Element of the carrier of L
n is set
L is non empty unital right_unital well-unital left_unital doubleLoopStr
1_ (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 is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
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
p is Relation-like n -defined Function-like total V208() finite-support set
(1_ (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
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
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) (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
(n,L,p) is Element of the carrier of L
p . (n,L,p) is Element of the carrier of L
p . (EmptyBag n) 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
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
the Relation-like n -defined Function-like Element of Support p is Relation-like n -defined Function-like Element of Support p
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
0. L is zero Element of the carrier of L
the ZeroF of L 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
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
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
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) (n,L) Element of bool [:(Bags n), the carrier of L:]
Support p is functional Element of bool (Bags n)
(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
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
a is set
Bags a is functional non empty Element of bool (Bags a)
Bags a is non empty set
bool (Bags a) is non empty set
x is non empty ZeroStr
the carrier of x is non empty set
[:(Bags a), the carrier of x:] is non empty set
bool [:(Bags a), the carrier of x:] 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) (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
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
y is Relation-like Bags a -defined the carrier of x -valued Function-like V18( Bags a, the carrier of x) finite-Support (a,x) (a,x) Element of bool [:(Bags a), the carrier of x:]
(a,x,y) is Element of the carrier of x
(a,x,y) is Relation-like a -defined Function-like total V208() finite-support set
y . (a,x,y) is Element of the carrier of x
EmptyBag a is Relation-like a -defined Function-like total V208() finite-support Element of Bags a
y . (EmptyBag a) is Element of the carrier of x
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) finite-Support (n,L) (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
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p is Element of the carrier of L
(0_ (n,L)) +* ((EmptyBag 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:]
L is non empty ZeroStr
the carrier of L is non empty set
n is set
p is Element of the carrier of L
(n,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:]
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) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag 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:]
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:]
(EmptyBag n) .--> p is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} is functional non empty trivial finite V36(1) set
{(EmptyBag n)} --> p is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {p} -valued Function-like constant non empty total V18({(EmptyBag n)},{p}) finite finite-support Element of bool [:{(EmptyBag n)},{p}:]
{p} is non empty trivial finite V36(1) set
[:{(EmptyBag n)},{p}:] is non empty finite set
bool [:{(EmptyBag n)},{p}:] is non empty finite V33() set
(0_ (n,L)) +* ((EmptyBag n) .--> p) is Relation-like Function-like set
q is Relation-like n -defined Function-like total V208() finite-support set
dom ((EmptyBag n) .--> p) is functional trivial finite Element of bool {(EmptyBag n)}
bool {(EmptyBag n)} is non empty finite V33() 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
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(n,L,(0. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) (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) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag n),(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:]
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:]
y is set
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)
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:]
(EmptyBag n) .--> (0. L) is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} is functional non empty trivial finite V36(1) set
{(EmptyBag n)} --> (0. L) is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {(0. L)} -valued Function-like constant non empty total V18({(EmptyBag n)},{(0. L)}) finite finite-support Element of bool [:{(EmptyBag n)},{(0. L)}:]
[:{(EmptyBag n)},{(0. L)}:] is non empty finite set
bool [:{(EmptyBag n)},{(0. L)}:] is non empty finite V33() set
(0_ (n,L)) +* ((EmptyBag n) .--> (0. L)) is Relation-like Function-like set
dom ((EmptyBag n) .--> (0. L)) is functional trivial finite Element of bool {(EmptyBag n)}
bool {(EmptyBag n)} is non empty finite V33() set
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
q . (EmptyBag n) is Element of the carrier of L
((0_ (n,L)) +* ((EmptyBag n) .--> (0. L))) . (EmptyBag n) is set
((EmptyBag n) .--> (0. L)) . (EmptyBag n) is set
r is Relation-like n -defined Function-like total V208() finite-support set
(n,L,(0. L)) . y is set
(0_ (n,L)) . y is set
r is Relation-like n -defined Function-like total V208() finite-support set
(n,L,(0. L)) . y is set
(0_ (n,L)) . y is set
r is Relation-like n -defined Function-like total V208() finite-support set
dom (n,L,(0. L)) is functional Element of bool (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) Element of bool [:(Bags n), 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 (n,L) (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
(n,L,(0. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag n),(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:]
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
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
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 (n,L) (n,L) Element of bool [:(Bags n), the carrier of L:]
p . (EmptyBag n) is Element of the carrier of L
(0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n))) 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:]
x is set
dom (0_ (n,L)) is functional Element of bool (Bags n)
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)
(EmptyBag n) .--> (p . (EmptyBag n)) is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} is functional non empty trivial finite V36(1) set
{(EmptyBag n)} --> (p . (EmptyBag n)) is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {(p . (EmptyBag n))} -valued Function-like constant non empty total V18({(EmptyBag n)},{(p . (EmptyBag n))}) finite finite-support Element of bool [:{(EmptyBag n)},{(p . (EmptyBag n))}:]
{(p . (EmptyBag n))} is non empty trivial finite V36(1) set
[:{(EmptyBag n)},{(p . (EmptyBag n))}:] is non empty finite set
bool [:{(EmptyBag n)},{(p . (EmptyBag n))}:] is non empty finite V33() set
(0_ (n,L)) +* ((EmptyBag n) .--> (p . (EmptyBag n))) is Relation-like Function-like set
dom ((EmptyBag n) .--> (p . (EmptyBag n))) is functional trivial finite Element of bool {(EmptyBag n)}
bool {(EmptyBag n)} is non empty finite V33() set
((0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n)))) . (EmptyBag n) is Element of the carrier of L
((0_ (n,L)) +* ((EmptyBag n) .--> (p . (EmptyBag n)))) . (EmptyBag n) is set
((EmptyBag n) .--> (p . (EmptyBag n))) . (EmptyBag n) is set
y is Relation-like n -defined Function-like total V208() finite-support set
p . x is set
((0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n)))) . x is set
y is Relation-like n -defined Function-like total V208() finite-support set
p . y is Element of the carrier of L
((0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n)))) . y is Element of the carrier of L
(0_ (n,L)) . y is Element of the carrier of L
p . x is set
((0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n)))) . x is set
y is Relation-like n -defined Function-like total V208() finite-support set
p . x is set
((0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n)))) . x is set
y is Relation-like n -defined Function-like total V208() finite-support set
p . x is set
((0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n)))) . x is set
dom ((0_ (n,L)) +* ((EmptyBag n),(p . (EmptyBag n)))) is functional Element of bool (Bags n)
(n,L,(p . (EmptyBag n))) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) (n,L) Element of bool [:(Bags n), the carrier of L:]
dom p is functional Element of bool (Bags n)
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 (n,L) (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
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
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 (n,L) (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
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
a is Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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:]
x is Element of the carrier of L
(n,L,x) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) (n,L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* ((EmptyBag 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:]
a is Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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:]
x is Element of the carrier of L
(n,L,x) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) (n,L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* ((EmptyBag 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:]
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 multLoopStr_0
the carrier of L 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
p is Element of the carrier of L
(n,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) (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) finite-Support (n,L) (n,L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* ((EmptyBag 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:]
(n,L,p) . (EmptyBag n) 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 (0_ (n,L)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
x is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p) . x is Element of the carrier of L
(0_ (n,L)) . 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
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(n,L,(0. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) (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) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag n),(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 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 unital right_unital well-unital left_unital multLoopStr_0
the carrier of L is non empty set
1. L is Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L,(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) (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) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag n),(1. 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:]
1_ (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:]
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:]
y is 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)
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:]
(EmptyBag n) .--> (1. L) is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} is functional non empty trivial finite V36(1) set
{(EmptyBag n)} --> (1. L) is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {(1. L)} -valued Function-like constant non empty total V18({(EmptyBag n)},{(1. L)}) finite finite-support Element of bool [:{(EmptyBag n)},{(1. L)}:]
{(1. L)} is non empty trivial finite V36(1) set
[:{(EmptyBag n)},{(1. L)}:] is non empty finite set
bool [:{(EmptyBag n)},{(1. L)}:] is non empty finite V33() set
(0_ (n,L)) +* ((EmptyBag n) .--> (1. L)) is Relation-like Function-like set
dom ((EmptyBag n) .--> (1. L)) is functional trivial finite Element of bool {(EmptyBag n)}
bool {(EmptyBag n)} is non empty finite V33() set
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
q . (EmptyBag n) is Element of the carrier of L
((0_ (n,L)) +* ((EmptyBag n) .--> (1. L))) . (EmptyBag n) is set
((EmptyBag n) .--> (1. L)) . (EmptyBag n) is set
r is Relation-like n -defined Function-like total V208() finite-support set
(n,L,(1. L)) . y is set
(1_ (n,L)) . y is set
r is Relation-like n -defined Function-like total V208() finite-support set
q . r is Element of the carrier of L
(0_ (n,L)) . r is Element of the carrier of L
(1_ (n,L)) . r is Element of the carrier of L
(n,L,(1. L)) . y is set
(1_ (n,L)) . y is set
r is Relation-like n -defined Function-like total V208() finite-support set
dom (n,L,(1. L)) is functional Element of bool (Bags n)
dom (1_ (n,L)) is functional Element of bool (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
p is Element of the carrier of L
(n,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) (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) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag 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:]
a is Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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:]
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:]
{(EmptyBag n)} is functional non empty trivial finite V36(1) set
(EmptyBag n) .--> p is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} --> p is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {p} -valued Function-like constant non empty total V18({(EmptyBag n)},{p}) finite finite-support Element of bool [:{(EmptyBag n)},{p}:]
{p} is non empty trivial finite V36(1) set
[:{(EmptyBag n)},{p}:] is non empty finite set
bool [:{(EmptyBag n)},{p}:] is non empty finite V33() set
dom ((EmptyBag n) .--> p) is functional trivial finite Element of bool {(EmptyBag n)}
bool {(EmptyBag n)} is non empty finite V33() set
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
bool (Bags n) is non empty set
(EmptyBag n) .--> a is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} --> a is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {a} -valued Function-like constant non empty total V18({(EmptyBag n)},{a}) finite finite-support Element of bool [:{(EmptyBag n)},{a}:]
{a} is non empty trivial finite V36(1) set
[:{(EmptyBag n)},{a}:] is non empty finite set
bool [:{(EmptyBag n)},{a}:] is non empty finite V33() set
dom ((EmptyBag n) .--> a) is functional trivial finite Element of bool {(EmptyBag n)}
dom (0_ (n,L)) is functional Element of bool (Bags n)
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)
i 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:]
i . (EmptyBag n) is Element of the carrier of L
(0_ (n,L)) +* ((EmptyBag n) .--> a) is Relation-like Function-like set
((0_ (n,L)) +* ((EmptyBag n) .--> a)) . (EmptyBag n) is set
((EmptyBag n) .--> a) . (EmptyBag n) 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:]
r . (EmptyBag n) is Element of the carrier of L
(0_ (n,L)) +* ((EmptyBag n) .--> p) is Relation-like Function-like set
((0_ (n,L)) +* ((EmptyBag n) .--> p)) . (EmptyBag n) is set
((EmptyBag n) .--> p) . (EmptyBag n) is 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
p is Element of the carrier of L
(n,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) (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) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag 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 (n,L,p) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
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
the carrier of L is non empty set
p is Element of the carrier of L
(n,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) (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) finite-Support (n,L) (n,L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* ((EmptyBag 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:]
(n,L,(n,L,p)) is Relation-like n -defined Function-like total V208() finite-support set
(n,L,(n,L,p)) is Element of the carrier of L
(n,L,p) . (n,L,(n,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:]
{(EmptyBag n)} is functional non empty trivial finite V36(1) set
(EmptyBag n) .--> p is Relation-like Bags n -defined {(EmptyBag n)} -defined the carrier of L -valued Function-like one-to-one finite finite-support set
{(EmptyBag n)} --> p is Relation-like {(EmptyBag n)} -defined the carrier of L -valued {p} -valued Function-like constant non empty total V18({(EmptyBag n)},{p}) finite finite-support Element of bool [:{(EmptyBag n)},{p}:]
{p} is non empty trivial finite V36(1) set
[:{(EmptyBag n)},{p}:] is non empty finite set
bool [:{(EmptyBag n)},{p}:] is non empty finite V33() set
dom ((EmptyBag n) .--> p) is functional trivial finite Element of bool {(EmptyBag n)}
bool {(EmptyBag n)} is non empty finite V33() set
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
bool (Bags n) is non empty set
dom (0_ (n,L)) is functional Element of bool (Bags n)
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)
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:]
z . (EmptyBag n) is Element of the carrier of L
(0_ (n,L)) +* ((EmptyBag n) .--> p) is Relation-like Function-like set
((0_ (n,L)) +* ((EmptyBag n) .--> p)) . (EmptyBag n) is set
((EmptyBag n) .--> p) . (EmptyBag n) is set
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 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 n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
[:n, the carrier of L:] is set
bool [: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) (n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p) is Relation-like n -defined Function-like total V208() finite-support set
p . (n,L,p) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval (p,a) 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 n)
bool (Bags n) is non empty set
BagOrder n is Relation-like Bags n -defined Bags n -valued total being_linear-order V197() V200() V204() Element of bool [:(Bags n),(Bags n):]
[:(Bags n),(Bags n):] is non empty set
bool [:(Bags n),(Bags n):] is non empty set
SgmX ((BagOrder n),(Support p)) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
len (SgmX ((BagOrder n),(Support p))) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
p * (SgmX ((BagOrder n),(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
x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
len x is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
Sum x 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
the Relation-like n -defined Function-like Element of Support p is Relation-like n -defined Function-like Element of Support p
z is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
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 n)
SgmX ((BagOrder n),y) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
<*> 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
y is functional finite Element of bool (Bags n)
SgmX ((BagOrder n),y) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
EmptyBag n is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
{(EmptyBag n)} is functional non empty trivial finite V36(1) Element of bool (Bags n)
r is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
rng (SgmX ((BagOrder n),y)) is set
dom (SgmX ((BagOrder n),y)) is Element of bool NAT
(SgmX ((BagOrder n),y)) . 1 is Relation-like Function-like 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 n),y)) /. q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(SgmX ((BagOrder n),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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT : ( 1 <= b₁ & b₁ <= r ) } is set
q is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(SgmX ((BagOrder n),y)) /. 1 is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
r is set
(SgmX ((BagOrder n),y)) /. 1 is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
len (SgmX ((BagOrder n),y)) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
dom p is functional Element of bool (Bags n)
p * (SgmX ((BagOrder n),y)) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
dom (p * (SgmX ((BagOrder n),y))) is Element of bool NAT
(p * (SgmX ((BagOrder n),y))) /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p * (SgmX ((BagOrder n),y))) . 1 is set
p . ((SgmX ((BagOrder n),y)) . 1) is set
p . (EmptyBag n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom x is Element of bool NAT
Seg (len x) is Element of bool NAT
x . 1 is set
x /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((SgmX ((BagOrder n),y)) /. 1) @ is Relation-like n -defined Function-like total V208() finite-support set
eval ((((SgmX ((BagOrder n),y)) /. 1) @),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((p * (SgmX ((BagOrder n),y))) /. 1) * (eval ((((SgmX ((BagOrder n),y)) /. 1) @),a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval ((EmptyBag n),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p) * (eval ((EmptyBag n),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
(n,L,p) * (1. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*(n,L,p)*> 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
n is epsilon-transitive epsilon-connected ordinal 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
[:n, the carrier of L:] is set
bool [:n, the carrier of L:] is non empty set
p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,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) (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) finite-Support (n,L) (n,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_ (n,L)) +* ((EmptyBag 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:]
a is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((n,L,p),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,(n,L,p)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,(n,L,p)) is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p) . (n,L,(n,L,p)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 multLoopStr_0
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
a 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:]
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:]
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 n -defined Function-like total V208() finite-support set
r . q is Element of the carrier of L
p . q is Element of the carrier of L
a * (p . q) 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:]
z is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
x . z is Element of the carrier of L
r is Relation-like n -defined Function-like total V208() finite-support set
p . r is Element of the carrier of L
a * (p . r) is Element of the carrier of L
y . z 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:]
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 n -defined Function-like total V208() finite-support set
r . q is Element of the carrier of L
p . q is Element of the carrier of L
(p . q) * a 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:]
z is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
x . z is Element of the carrier of L
r is Relation-like n -defined Function-like total V208() finite-support set
p . r is Element of the carrier of L
(p . r) * a is Element of the carrier of L
y . z 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 left_add-cancelable right_add-cancelable add-cancelable right_zeroed right-distributive left-distributive distributive left_zeroed doubleLoopStr
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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
(n,L,p,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 set
Support (n,L,p,a) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
(n,L,p,a) . y is set
0. L is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
the ZeroF of L is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
z is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . z is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
a * (p . z) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
Support p is functional Element of bool (Bags n)
(n,L,p,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 set
Support (n,L,p,a) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
(n,L,p,a) . y is set
0. L is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
the ZeroF of L is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
z is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . z is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
(p . z) * a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of L
Support p is functional Element of bool (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 commutative multLoopStr_0
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:]
a is Element of the carrier of L
(n,L,p,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:]
(n,L,p,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:]
x is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(n,L,p,a) . x is Element of the carrier of L
y is Relation-like n -defined Function-like total V208() finite-support set
p . y is Element of the carrier of L
a * (p . y) is Element of the carrier of L
(n,L,p,a) . x 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 left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left-distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,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:]
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
(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:]
z is set
(n,L,p,a) . z is set
((n,L,a) *' p) . z is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
((n,L,a) *' p) . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (p . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
decomp q is Relation-like NAT -defined K469(2,(Bags n)) -valued Function-like one-to-one non empty FinSequence-like Function-yielding V159() FinSequence-yielding FinSequence of K469(2,(Bags n))
K469(2,(Bags n)) is M35( Bags n)
len (decomp q) is non empty 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
Sum r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len r is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
dom r is Element of bool NAT
r . 1 is set
q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*q*> 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 NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
<*q*> ^ i is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
Sum <*q*> is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Sum i is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum <*q*>) + (Sum i) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*> 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))
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
<*> 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))
len i is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
len <*q*> is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(len i) + (len <*q*>) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(len i) + 1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() set
dom i is Element of bool NAT
i /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
i . k is set
k + 1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
r . (k + 1) is set
dom (decomp q) is Element of bool NAT
r /. (k + 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
c + 1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(decomp q) /. (c + 1) is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
r /. (c + 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is Relation-like n -defined Function-like total V208() finite-support set
b2 is Relation-like n -defined Function-like total V208() finite-support set
<*c,b2*> is set
(n,L,a) . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . b2 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((n,L,a) . c) * (p . b2) 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
(0. L) * (p . b2) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
[:NAT,(Bags n):] is non empty non trivial non finite set
bool [:NAT,(Bags n):] is non empty non trivial non finite set
<*(EmptyBag n),(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() M36( Bags n,K468((Bags n)))
K468((Bags n)) is M35( Bags n)
<*<*(EmptyBag n),(EmptyBag n)*>*> is Relation-like NAT -defined bool [:NAT,(Bags n):] -valued Function-like FinSequence-like Function-yielding V159() FinSequence-yielding M36( bool [:NAT,(Bags n):],K468((bool [:NAT,(Bags n):])))
K468((bool [:NAT,(Bags n):])) is M35( bool [:NAT,(Bags n):])
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(decomp q) /. (k + 1) is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
c is Relation-like n -defined Function-like total V208() finite-support set
c is Relation-like n -defined Function-like total V208() finite-support set
<*c,c*> is set
(n,L,a) . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((n,L,a) . c) * (p . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(decomp q) /. (len r) is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
<*q,(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() M36( Bags n,K468((Bags n)))
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
p . (EmptyBag n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(0. L) * (p . (EmptyBag n)) 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
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
<*> 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))
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
(decomp q) /. 1 is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
r /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k is Relation-like n -defined Function-like total V208() finite-support set
c is Relation-like n -defined Function-like total V208() finite-support set
<*k,c*> is set
(n,L,a) . k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((n,L,a) . k) * (p . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*(EmptyBag n),q*> is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() M36( Bags n,K468((Bags n)))
K468((Bags n)) is M35( Bags n)
r is Relation-like n -defined Function-like total V208() finite-support set
((n,L,a) *' p) . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (p . r) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,a) . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom (n,L,p,a) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
dom ((n,L,a) *' p) is functional Element of bool (Bags n)
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 left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed right-distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,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:]
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
p *' (n,L,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:]
z is set
(n,L,p,a) . z is set
(p *' (n,L,a)) . z is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
(p *' (n,L,a)) . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . q) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
decomp q is Relation-like NAT -defined K469(2,(Bags n)) -valued Function-like one-to-one non empty FinSequence-like Function-yielding V159() FinSequence-yielding FinSequence of K469(2,(Bags n))
K469(2,(Bags n)) is M35( Bags n)
len (decomp q) is non empty 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
Sum r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
len r is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
dom r is Element of bool NAT
q is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
i is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*i*> 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)
q ^ <*i*> is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
<*> 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))
Sum q 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
<*> 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))
len q is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
len <*i*> is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(len q) + (len <*i*>) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(len q) + 1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() set
dom q is Element of bool NAT
q /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q . k is set
r . k is set
dom (decomp q) is Element of bool NAT
r /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(decomp q) /. c is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
r /. c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is Relation-like n -defined Function-like total V208() finite-support set
b2 is Relation-like n -defined Function-like total V208() finite-support set
<*c,b2*> is set
p . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,a) . b2 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . c) * ((n,L,a) . b2) 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
(p . c) * (0. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
[:NAT,(Bags n):] is non empty non trivial non finite set
bool [:NAT,(Bags n):] is non empty non trivial non finite set
<*(EmptyBag n),(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() M36( Bags n,K468((Bags n)))
K468((Bags n)) is M35( Bags n)
<*<*(EmptyBag n),(EmptyBag n)*>*> is Relation-like NAT -defined bool [:NAT,(Bags n):] -valued Function-like FinSequence-like Function-yielding V159() FinSequence-yielding M36( bool [:NAT,(Bags n):],K468((bool [:NAT,(Bags n):])))
K468((bool [:NAT,(Bags n):])) is M35( bool [:NAT,(Bags n):])
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(decomp q) /. k is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
c is Relation-like n -defined Function-like total V208() finite-support set
c is Relation-like n -defined Function-like total V208() finite-support set
<*c,c*> is set
p . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,a) . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . c) * ((n,L,a) . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(decomp q) /. 1 is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
<*(EmptyBag n),q*> is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() M36( Bags n,K468((Bags n)))
p . (EmptyBag n) 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
(p . (EmptyBag n)) * (0. 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
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
Sum q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*> 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))
Sum q 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
Sum q 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
r . (len r) is set
len q is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(len q) + 1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(q ^ <*i*>) . ((len q) + 1) is set
Sum <*i*> is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(Sum q) + (Sum <*i*>) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(decomp q) /. (len r) is Relation-like Bags n -valued Function-like FinSequence-like Function-yielding V159() Element of K469(2,(Bags n))
r /. (len r) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k is Relation-like n -defined Function-like total V208() finite-support set
c is Relation-like n -defined Function-like total V208() finite-support set
<*k,c*> is set
p . k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,a) . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . k) * ((n,L,a) . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*q,(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() M36( Bags n,K468((Bags n)))
K468((Bags n)) is M35( Bags n)
r is Relation-like n -defined Function-like total V208() finite-support set
(p *' (n,L,a)) . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . r) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,a) . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom (n,L,p,a) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
dom (p *' (n,L,a)) is functional Element of bool (Bags n)
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 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 left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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
[:n, the carrier of L:] is set
bool [: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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
(n,L,a) *' p 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:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval (((n,L,a) *' p),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (eval (p,x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval ((n,L,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(eval ((n,L,a),x)) * (eval (p,x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 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 left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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
[:n, the carrier of L:] is set
bool [: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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
p *' (n,L,a) 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:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((p *' (n,L,a)),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(eval (p,x)) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval ((n,L,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(eval (p,x)) * (eval ((n,L,a),x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 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 left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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
[:n, the carrier of L:] is set
bool [: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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(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 Element of bool [:(Bags n), the carrier of L:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((n,L,p,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (eval (p,x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
(n,L,a) *' p 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:]
eval (((n,L,a) *' p),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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
[:n, the carrier of L:] is set
bool [: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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(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 Element of bool [:(Bags n), the carrier of L:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((n,L,p,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (eval (p,x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Support (n,L,p,a) is functional finite Element of bool (Bags n)
bool (Bags n) is non empty set
BagOrder n is Relation-like Bags n -defined Bags n -valued total being_linear-order V197() V200() V204() Element of bool [:(Bags n),(Bags n):]
[:(Bags n),(Bags n):] is non empty set
bool [:(Bags n),(Bags n):] is non empty set
SgmX ((BagOrder n),(Support (n,L,p,a))) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
len (SgmX ((BagOrder n),(Support (n,L,p,a)))) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(n,L,p,a) * (SgmX ((BagOrder n),(Support (n,L,p,a)))) 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
y is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
len y is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
Sum y 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 n)
SgmX ((BagOrder n),(Support p)) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
len (SgmX ((BagOrder n),(Support p))) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
p * (SgmX ((BagOrder n),(Support p))) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
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
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
r is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p,a) . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (p . r) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is functional non empty Element of bool (Bags n)
the Relation-like n -defined Function-like total V208() finite-support Element of r is Relation-like n -defined Function-like total V208() finite-support Element of r
(n,L,p,a) . the Relation-like n -defined Function-like total V208() finite-support Element of r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
rng (SgmX ((BagOrder n),(Support (n,L,p,a)))) is set
<*> 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)
a * (Sum z) 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
r is set
(n,L,p,a) . r is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (p . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is set
p . r is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (p . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,a) . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom z is Element of bool NAT
Seg (len y) is Element of bool NAT
dom y is Element of bool NAT
dom (n,L,p,a) is functional Element of bool (Bags n)
r is set
rng (SgmX ((BagOrder n),(Support (n,L,p,a)))) is set
r is Relation-like Function-like FinSequence-like set
rng r is set
q is set
rng (n,L,p,a) is set
dom p is functional Element of bool (Bags n)
q is set
p * (SgmX ((BagOrder n),(Support (n,L,p,a)))) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
q is Relation-like Function-like FinSequence-like set
rng q is set
r is set
rng p is set
i is set
Seg (len z) is Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT : ( 1 <= b₁ & b₁ <= len z ) } is set
k is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
Seg (len (SgmX ((BagOrder n),(Support (n,L,p,a))))) is Element of bool NAT
dom (SgmX ((BagOrder n),(Support (n,L,p,a)))) is Element of bool NAT
(SgmX ((BagOrder n),(Support (n,L,p,a)))) . k is Relation-like Function-like set
(SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
q is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom q is Element of bool NAT
(p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q . k is set
p . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) . k) is set
p . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
z /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (z /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p * (SgmX ((BagOrder n),(Support p)))) /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(SgmX ((BagOrder n),(Support p))) /. k is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
((SgmX ((BagOrder n),(Support p))) /. k) @ is Relation-like n -defined Function-like total V208() finite-support set
eval ((((SgmX ((BagOrder n),(Support p))) /. k) @),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((p * (SgmX ((BagOrder n),(Support p)))) /. k) * (eval ((((SgmX ((BagOrder n),(Support p))) /. k) @),x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (((p * (SgmX ((BagOrder n),(Support p)))) /. k) * (eval ((((SgmX ((BagOrder n),(Support p))) /. k) @),x))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * ((p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @ is Relation-like n -defined Function-like total V208() finite-support set
eval ((((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(a * ((p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k)) * (eval ((((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @),x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,a) . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p,a) . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom r is Element of bool NAT
((n,L,p,a) * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . k is set
(n,L,p,a) . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) . k) is set
y /. i is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
z /. i is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (z /. i) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * z is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence 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
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 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 left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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
[:n, the carrier of L:] is set
bool [: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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(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 Element of bool [:(Bags n), the carrier of L:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((n,L,p,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(eval (p,x)) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
p *' (n,L,a) 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:]
eval ((p *' (n,L,a)),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable 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
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
[:n, the carrier of L:] is set
bool [: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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(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 Element of bool [:(Bags n), the carrier of L:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((n,L,p,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(eval (p,x)) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
Support (n,L,p,a) is functional finite Element of bool (Bags n)
bool (Bags n) is non empty set
BagOrder n is Relation-like Bags n -defined Bags n -valued total being_linear-order V197() V200() V204() Element of bool [:(Bags n),(Bags n):]
[:(Bags n),(Bags n):] is non empty set
bool [:(Bags n),(Bags n):] is non empty set
SgmX ((BagOrder n),(Support (n,L,p,a))) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
len (SgmX ((BagOrder n),(Support (n,L,p,a)))) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
(n,L,p,a) * (SgmX ((BagOrder n),(Support (n,L,p,a)))) 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
y is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
len y is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
Sum y 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 n)
SgmX ((BagOrder n),(Support p)) is Relation-like NAT -defined Bags n -valued Function-like FinSequence-like Function-yielding V159() FinSequence of Bags n
len (SgmX ((BagOrder n),(Support p))) is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
p * (SgmX ((BagOrder n),(Support p))) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
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
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
r is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p,a) . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
p . r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . r) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is functional non empty Element of bool (Bags n)
the Relation-like n -defined Function-like total V208() finite-support Element of r is Relation-like n -defined Function-like total V208() finite-support Element of r
(n,L,p,a) . the Relation-like n -defined Function-like total V208() finite-support Element of r is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
rng (SgmX ((BagOrder n),(Support (n,L,p,a)))) is set
<*> 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)
(Sum z) * a 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
r is set
(n,L,p,a) . r is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . q) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is set
p . r is set
q is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
p . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p . q) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,a) . q is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
dom z is Element of bool NAT
Seg (len y) is Element of bool NAT
dom y is Element of bool NAT
dom (n,L,p,a) is functional Element of bool (Bags n)
r is set
rng (SgmX ((BagOrder n),(Support (n,L,p,a)))) is set
r is Relation-like Function-like FinSequence-like set
rng r is set
q is set
rng (n,L,p,a) is set
dom p is functional Element of bool (Bags n)
q is set
p * (SgmX ((BagOrder n),(Support (n,L,p,a)))) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
q is Relation-like Function-like FinSequence-like set
rng q is set
r is set
rng p is set
i is set
Seg (len z) is Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT : ( 1 <= b₁ & b₁ <= len z ) } is set
k is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT
Seg (len (SgmX ((BagOrder n),(Support (n,L,p,a))))) is Element of bool NAT
dom (SgmX ((BagOrder n),(Support (n,L,p,a)))) is Element of bool NAT
(SgmX ((BagOrder n),(Support (n,L,p,a)))) . k is Relation-like Function-like set
(SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
q is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom q is Element of bool NAT
(p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
q . k is set
p . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) . k) is set
p . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is Relation-like n -defined Function-like total V208() finite-support Element of Bags n
z /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(z /. k) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @ is Relation-like n -defined Function-like total V208() finite-support set
eval ((((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k) * (eval ((((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @),x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(((p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k) * (eval ((((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @),x))) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(((p * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k) * a) * (eval ((((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) @),x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,p,a) . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) /. k) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
c is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p,a) . c is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom r is Element of bool NAT
((n,L,p,a) * (SgmX ((BagOrder n),(Support (n,L,p,a))))) /. k is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r . k is set
(n,L,p,a) . ((SgmX ((BagOrder n),(Support (n,L,p,a)))) . k) is set
y /. i is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
z /. i is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(z /. i) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
z * a is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence 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
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
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 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 left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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
[:n, the carrier of L:] is set
bool [:n, the carrier of L:] is non empty set
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
p 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,L,a) *' p 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:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval (((n,L,a) *' p),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
a * (eval (p,x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable 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 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 left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
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
[:n, the carrier of L:] is set
bool [: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 Element of bool [:(Bags n), the carrier of L:]
a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(n,L,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) (n,L) Element of bool [:(Bags n), 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 (n,L) (n,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_ (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:]
p *' (n,L,a) 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:]
x is Relation-like n -defined the carrier of L -valued Function-like V18(n, the carrier of L) Element of bool [:n, the carrier of L:]
eval ((p *' (n,L,a)),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval (p,x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(eval (p,x)) * a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
eval ((n,L,a),x) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(eval (p,x)) * (eval ((n,L,a),x)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L