:: POLYNOM1 semantic presentation

REAL is V62() V63() V64() V68() set
NAT is non trivial ordinal non finite V38() V39() V62() V63() V64() V65() V66() V67() V68() Element of bool REAL
bool REAL is non empty set
NAT is non trivial ordinal non finite V38() V39() V62() V63() V64() V65() V66() V67() V68() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is V62() V68() set
RAT is V62() V63() V64() V65() V68() set
INT is V62() V63() V64() V65() V66() V68() set
{} is set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support set
1 is non empty ordinal natural finite V38() V45() V46() ext-real positive V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
{{},1} is finite set
2 is non empty ordinal natural finite V38() V45() V46() ext-real positive V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
[:NAT,REAL:] is Relation-like V52() V53() V54() set
bool [:NAT,REAL:] is non empty set
3 is non empty ordinal natural finite V38() V45() V46() ext-real positive V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
0 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
Seg 1 is non empty trivial finite V40(1) V62() V63() V64() V65() V66() V67() Element of bool NAT
{1} is non empty trivial finite V37() V40(1) V62() V63() V64() V65() V66() V67() set
Seg 2 is non empty finite V40(2) V62() V63() V64() V65() V66() V67() Element of bool NAT
{1,2} is finite V37() V62() V63() V64() V65() V66() V67() set
n is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive right_unital add-associative right_zeroed doubleLoopStr
0. n is V82(n) Element of the carrier of n
the carrier of n is non empty set
the ZeroF of n is Element of the carrier of n
1. n is Element of the carrier of n
the OneF of n is Element of the carrier of n
L is Element of the carrier of n
L * (1. n) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (L,(1. n)) is Element of the carrier of n
n is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive right_unital add-associative right_zeroed doubleLoopStr
n is non empty addLoopStr
the carrier of n is non empty set
L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom L is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom Pm is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
L + Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom (L + Pm) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
<:L,Pm:> is Relation-like Function-like set
rng <:L,Pm:> is set
rng L is finite Element of bool the carrier of n
bool the carrier of n is non empty set
rng Pm is finite Element of bool the carrier of n
[:(rng L),(rng Pm):] is Relation-like finite set
[: the carrier of n, the carrier of n:] is Relation-like non empty set
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
dom the addF of n is Relation-like the carrier of n -defined the carrier of n -valued non empty Element of bool [: the carrier of n, the carrier of n:]
bool [: the carrier of n, the carrier of n:] is non empty set
the addF of n .: (L,Pm) is Relation-like Function-like set
<:L,Pm:> * the addF of n is Relation-like the carrier of n -valued Function-like set
dom ( the addF of n .: (L,Pm)) is set
dom <:L,Pm:> is set
(dom L) /\ (dom Pm) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
n is non empty addLoopStr
the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Relation-like NAT -defined the carrier of n * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of n *
Sum L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom (Sum L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom L is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len (Sum L) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len L is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
n is non empty addLoopStr
the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
<*> ( the carrier of n *) is Relation-like non-empty empty-yielding NAT -defined the carrier of n * -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of ( the carrier of n *) *
( the carrier of n *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n *
Sum (<*> ( the carrier of n *)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of n *
dom (Sum (<*> ( the carrier of n *))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (<*> ( the carrier of n *)) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of bool NAT
n is non empty addLoopStr
the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum L is Element of the carrier of n
<*(Sum L)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
<*L*> is Relation-like NAT -defined the carrier of n * -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of ( the carrier of n *) *
( the carrier of n *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n *
Sum <*L*> is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Pm is ordinal natural finite V38() V45() V46() ext-real set
dom <*L*> is non empty trivial finite V40(1) V62() V63() V64() V65() V66() V67() Element of bool NAT
<*(Sum L)*> /. Pm is Element of the carrier of n
<*L*> /. Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum (<*L*> /. Pm) is Element of the carrier of n
dom <*(Sum L)*> is non empty trivial finite V40(1) V62() V63() V64() V65() V66() V67() Element of bool NAT
len <*(Sum L)*> is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len <*L*> is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
n is non empty addLoopStr
the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Relation-like NAT -defined the carrier of n * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of n *
Pm is Relation-like NAT -defined the carrier of n * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of n *
L ^ Pm is Relation-like NAT -defined the carrier of n * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of n *
Sum (L ^ Pm) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(Sum L) ^ (Sum Pm) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom (Sum L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom L is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (Sum Pm) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom Pm is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len ((Sum L) ^ (Sum Pm)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len (Sum L) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len (Sum Pm) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len (Sum L)) + (len (Sum Pm)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len L is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len L) + (len (Sum Pm)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len Pm is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len L) + (len Pm) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len (L ^ Pm) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom ((Sum L) ^ (Sum Pm)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (L ^ Pm) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
x is ordinal natural finite V38() V45() V46() ext-real set
((Sum L) ^ (Sum Pm)) /. x is Element of the carrier of n
((Sum L) ^ (Sum Pm)) . x is set
(Sum L) . x is set
(Sum L) /. x is Element of the carrier of n
L /. x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum (L /. x) is Element of the carrier of n
(L ^ Pm) /. x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum ((L ^ Pm) /. x) is Element of the carrier of n
y is ordinal natural finite V38() V45() V46() ext-real set
(len L) + y is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
y is ordinal natural finite V38() V45() V46() ext-real set
(len L) + y is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
((Sum L) ^ (Sum Pm)) /. x is Element of the carrier of n
((Sum L) ^ (Sum Pm)) . x is set
(Sum Pm) . y is set
(Sum Pm) /. y is Element of the carrier of n
Pm /. y is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum (Pm /. y) is Element of the carrier of n
(L ^ Pm) /. x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum ((L ^ Pm) /. x) is Element of the carrier of n
n is non empty multMagma
the carrier of n is non empty set
L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Pm is Element of the carrier of n
Pm * L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom L is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
Pm multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
bool [: the carrier of n, the carrier of n:] is non empty set
(Pm multfield) * L is Relation-like NAT -defined the carrier of n -valued Function-like finite finite-support Element of bool [:NAT, the carrier of n:]
[:NAT, the carrier of n:] is Relation-like non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial non finite set
y is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom y is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
z is set
y . z is set
((Pm multfield) * L) . z is set
y /. z is Element of the carrier of n
L /. z is Element of the carrier of n
Pm * (L /. z) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (Pm,(L /. z)) is Element of the carrier of n
(Pm multfield) . (L /. z) is Element of the carrier of n
L . z is set
(Pm multfield) . (L . z) is set
rng L is finite Element of bool the carrier of n
bool the carrier of n is non empty set
dom (Pm multfield) is non empty Element of bool the carrier of n
dom ((Pm multfield) * L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
y is set
dom (Pm * L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
y is set
(Pm * L) /. y is Element of the carrier of n
L /. y is Element of the carrier of n
Pm * (L /. y) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (Pm,(L /. y)) is Element of the carrier of n
(Pm * L) . y is set
((Pm multfield) * L) . y is set
L . y is set
(Pm multfield) . (L . y) is set
(Pm multfield) . (L /. y) is Element of the carrier of n
y is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom y is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
z is set
y /. z is Element of the carrier of n
L /. z is Element of the carrier of n
Pm * (L /. z) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (Pm,(L /. z)) is Element of the carrier of n
p is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom p is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
n is non empty multMagma
the carrier of n is non empty set
L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom L is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
Pm is Element of the carrier of n
len L is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
len x is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom x is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
y is set
x /. y is Element of the carrier of n
L /. y is Element of the carrier of n
(L /. y) * Pm is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . ((L /. y),Pm) is Element of the carrier of n
x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom x is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
y is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom y is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
z is ordinal natural finite V38() V45() V46() ext-real set
x /. z is Element of the carrier of n
L /. z is Element of the carrier of n
(L /. z) * Pm is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . ((L /. z),Pm) is Element of the carrier of n
y /. z is Element of the carrier of n
n is non empty multMagma
the carrier of n is non empty set
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of n *
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Element of the carrier of n
L * (<*> the carrier of n) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom (L * (<*> the carrier of n)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (<*> the carrier of n) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of bool NAT
n is non empty multMagma
the carrier of n is non empty set
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of n *
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Element of the carrier of n
(n,(<*> the carrier of n),L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom (n,(<*> the carrier of n),L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (<*> the carrier of n) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of bool NAT
n is non empty multMagma
the carrier of n is non empty set
Pm is Element of the carrier of n
<*Pm*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Element of the carrier of n
L * <*Pm*> is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
L * Pm is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (L,Pm) is Element of the carrier of n
<*(L * Pm)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
dom <*Pm*> is non empty trivial finite V40(1) V62() V63() V64() V65() V66() V67() Element of bool NAT
x is set
<*(L * Pm)*> /. x is Element of the carrier of n
<*Pm*> /. x is Element of the carrier of n
L * (<*Pm*> /. x) is Element of the carrier of n
the multF of n . (L,(<*Pm*> /. x)) is Element of the carrier of n
dom <*(L * Pm)*> is non empty trivial finite V40(1) V62() V63() V64() V65() V66() V67() Element of bool NAT
n is non empty multMagma
the carrier of n is non empty set
Pm is Element of the carrier of n
<*Pm*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Element of the carrier of n
(n,<*Pm*>,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Pm * L is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (Pm,L) is Element of the carrier of n
<*(Pm * L)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
dom <*Pm*> is non empty trivial finite V40(1) V62() V63() V64() V65() V66() V67() Element of bool NAT
x is set
<*(Pm * L)*> /. x is Element of the carrier of n
<*Pm*> /. x is Element of the carrier of n
(<*Pm*> /. x) * L is Element of the carrier of n
the multF of n . ((<*Pm*> /. x),L) is Element of the carrier of n
dom <*(Pm * L)*> is non empty trivial finite V40(1) V62() V63() V64() V65() V66() V67() Element of bool NAT
n is non empty multMagma
the carrier of n is non empty set
L is Element of the carrier of n
Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Pm ^ x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
L * (Pm ^ x) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
L * Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
L * x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(L * Pm) ^ (L * x) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom (L * (Pm ^ x)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (Pm ^ x) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (L * x) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom x is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len (L * x) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len x is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom (L * Pm) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom Pm is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len (L * Pm) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len Pm is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
y is ordinal natural finite V38() V45() V46() ext-real set
(L * (Pm ^ x)) /. y is Element of the carrier of n
(Pm ^ x) /. y is Element of the carrier of n
L * ((Pm ^ x) /. y) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (L,((Pm ^ x) /. y)) is Element of the carrier of n
Pm /. y is Element of the carrier of n
L * (Pm /. y) is Element of the carrier of n
the multF of n . (L,(Pm /. y)) is Element of the carrier of n
(L * Pm) /. y is Element of the carrier of n
((L * Pm) ^ (L * x)) /. y is Element of the carrier of n
z is ordinal natural finite V38() V45() V46() ext-real set
(len Pm) + z is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
z is ordinal natural finite V38() V45() V46() ext-real set
(len Pm) + z is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(L * (Pm ^ x)) /. y is Element of the carrier of n
(Pm ^ x) /. y is Element of the carrier of n
L * ((Pm ^ x) /. y) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (L,((Pm ^ x) /. y)) is Element of the carrier of n
x /. z is Element of the carrier of n
L * (x /. z) is Element of the carrier of n
the multF of n . (L,(x /. z)) is Element of the carrier of n
(L * x) /. z is Element of the carrier of n
((L * Pm) ^ (L * x)) /. y is Element of the carrier of n
len ((L * Pm) ^ (L * x)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len (L * Pm)) + (len (L * x)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len (Pm ^ x) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom ((L * Pm) ^ (L * x)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
n is non empty multMagma
the carrier of n is non empty set
L is Element of the carrier of n
Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Pm ^ x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(n,(Pm ^ x),L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(n,Pm,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(n,x,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(n,Pm,L) ^ (n,x,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
dom (n,(Pm ^ x),L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (Pm ^ x) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (n,x,L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom x is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len (n,x,L) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len x is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom (n,Pm,L) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom Pm is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len (n,Pm,L) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len Pm is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
y is ordinal natural finite V38() V45() V46() ext-real set
(n,(Pm ^ x),L) /. y is Element of the carrier of n
(Pm ^ x) /. y is Element of the carrier of n
((Pm ^ x) /. y) * L is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (((Pm ^ x) /. y),L) is Element of the carrier of n
Pm /. y is Element of the carrier of n
(Pm /. y) * L is Element of the carrier of n
the multF of n . ((Pm /. y),L) is Element of the carrier of n
(n,Pm,L) /. y is Element of the carrier of n
((n,Pm,L) ^ (n,x,L)) /. y is Element of the carrier of n
z is ordinal natural finite V38() V45() V46() ext-real set
(len Pm) + z is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
z is ordinal natural finite V38() V45() V46() ext-real set
(len Pm) + z is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(n,(Pm ^ x),L) /. y is Element of the carrier of n
(Pm ^ x) /. y is Element of the carrier of n
((Pm ^ x) /. y) * L is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (((Pm ^ x) /. y),L) is Element of the carrier of n
x /. z is Element of the carrier of n
(x /. z) * L is Element of the carrier of n
the multF of n . ((x /. z),L) is Element of the carrier of n
(n,x,L) /. z is Element of the carrier of n
((n,Pm,L) ^ (n,x,L)) /. y is Element of the carrier of n
len ((n,Pm,L) ^ (n,x,L)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len (n,Pm,L)) + (len (n,x,L)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len (Pm ^ x) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom ((n,Pm,L) ^ (n,x,L)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
multEX_0 is non empty strict almost_cancelable almost_invertible multLoop_0-like unital associative right_unital well-unital left_unital multLoopStr_0
F_Real is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible strict left_zeroed add-left-invertible add-right-invertible Loop-like unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
n is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
the carrier of n is non empty set
L is Element of the carrier of n
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of n *
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
L * x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (L * x) is Element of the carrier of n
Sum x is Element of the carrier of n
L * (Sum x) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (L,(Sum x)) is Element of the carrier of n
y is Element of the carrier of n
<*y*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
x ^ <*y*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
L * (x ^ <*y*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (L * (x ^ <*y*>)) is Element of the carrier of n
L * <*y*> is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(L * x) ^ (L * <*y*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum ((L * x) ^ (L * <*y*>)) is Element of the carrier of n
Sum (L * <*y*>) is Element of the carrier of n
(Sum (L * x)) + (Sum (L * <*y*>)) is Element of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
the addF of n . ((Sum (L * x)),(Sum (L * <*y*>))) is Element of the carrier of n
L * y is Element of the carrier of n
the multF of n . (L,y) is Element of the carrier of n
<*(L * y)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum <*(L * y)*> is Element of the carrier of n
(Sum (L * x)) + (Sum <*(L * y)*>) is Element of the carrier of n
the addF of n . ((Sum (L * x)),(Sum <*(L * y)*>)) is Element of the carrier of n
(Sum (L * x)) + (L * y) is Element of the carrier of n
the addF of n . ((Sum (L * x)),(L * y)) is Element of the carrier of n
Sum <*y*> is Element of the carrier of n
L * (Sum <*y*>) is Element of the carrier of n
the multF of n . (L,(Sum <*y*>)) is Element of the carrier of n
(L * (Sum x)) + (L * (Sum <*y*>)) is Element of the carrier of n
the addF of n . ((L * (Sum x)),(L * (Sum <*y*>))) is Element of the carrier of n
(Sum x) + (Sum <*y*>) is Element of the carrier of n
the addF of n . ((Sum x),(Sum <*y*>)) is Element of the carrier of n
L * ((Sum x) + (Sum <*y*>)) is Element of the carrier of n
the multF of n . (L,((Sum x) + (Sum <*y*>))) is Element of the carrier of n
Sum (x ^ <*y*>) is Element of the carrier of n
L * (Sum (x ^ <*y*>)) is Element of the carrier of n
the multF of n . (L,(Sum (x ^ <*y*>))) is Element of the carrier of n
Sum (<*> the carrier of n) is Element of the carrier of n
0. n is V82(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
L * (<*> the carrier of n) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (L * (<*> the carrier of n)) is Element of the carrier of n
L * (Sum (<*> the carrier of n)) is Element of the carrier of n
the multF of n . (L,(Sum (<*> the carrier of n))) is Element of the carrier of n
n is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
the carrier of n is non empty set
L is Element of the carrier of n
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of n *
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(n,x,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (n,x,L) is Element of the carrier of n
Sum x is Element of the carrier of n
(Sum x) * L is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . ((Sum x),L) is Element of the carrier of n
y is Element of the carrier of n
<*y*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
x ^ <*y*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(n,(x ^ <*y*>),L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (n,(x ^ <*y*>),L) is Element of the carrier of n
(n,<*y*>,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(n,x,L) ^ (n,<*y*>,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum ((n,x,L) ^ (n,<*y*>,L)) is Element of the carrier of n
Sum (n,<*y*>,L) is Element of the carrier of n
(Sum (n,x,L)) + (Sum (n,<*y*>,L)) is Element of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
the addF of n . ((Sum (n,x,L)),(Sum (n,<*y*>,L))) is Element of the carrier of n
y * L is Element of the carrier of n
the multF of n . (y,L) is Element of the carrier of n
<*(y * L)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum <*(y * L)*> is Element of the carrier of n
(Sum (n,x,L)) + (Sum <*(y * L)*>) is Element of the carrier of n
the addF of n . ((Sum (n,x,L)),(Sum <*(y * L)*>)) is Element of the carrier of n
(Sum (n,x,L)) + (y * L) is Element of the carrier of n
the addF of n . ((Sum (n,x,L)),(y * L)) is Element of the carrier of n
Sum <*y*> is Element of the carrier of n
(Sum <*y*>) * L is Element of the carrier of n
the multF of n . ((Sum <*y*>),L) is Element of the carrier of n
((Sum x) * L) + ((Sum <*y*>) * L) is Element of the carrier of n
the addF of n . (((Sum x) * L),((Sum <*y*>) * L)) is Element of the carrier of n
(Sum x) + (Sum <*y*>) is Element of the carrier of n
the addF of n . ((Sum x),(Sum <*y*>)) is Element of the carrier of n
((Sum x) + (Sum <*y*>)) * L is Element of the carrier of n
the multF of n . (((Sum x) + (Sum <*y*>)),L) is Element of the carrier of n
Sum (x ^ <*y*>) is Element of the carrier of n
(Sum (x ^ <*y*>)) * L is Element of the carrier of n
the multF of n . ((Sum (x ^ <*y*>)),L) is Element of the carrier of n
Sum (<*> the carrier of n) is Element of the carrier of n
0. n is V82(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
(n,(<*> the carrier of n),L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (n,(<*> the carrier of n),L) is Element of the carrier of n
(Sum (<*> the carrier of n)) * L is Element of the carrier of n
the multF of n . ((Sum (<*> the carrier of n)),L) is Element of the carrier of n
n is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Relation-like NAT -defined the carrier of n * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of n *
FlattenSeq L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum (FlattenSeq L) is Element of the carrier of n
Sum L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (Sum L) is Element of the carrier of n
Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
<*Pm*> is Relation-like NAT -defined the carrier of n * -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of ( the carrier of n *) *
( the carrier of n *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n *
L ^ <*Pm*> is Relation-like NAT -defined the carrier of n * -valued Function-like non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of n *
FlattenSeq (L ^ <*Pm*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum (FlattenSeq (L ^ <*Pm*>)) is Element of the carrier of n
Sum (L ^ <*Pm*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (Sum (L ^ <*Pm*>)) is Element of the carrier of n
FlattenSeq <*Pm*> is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
(FlattenSeq L) ^ (FlattenSeq <*Pm*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum ((FlattenSeq L) ^ (FlattenSeq <*Pm*>)) is Element of the carrier of n
(FlattenSeq L) ^ Pm is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum ((FlattenSeq L) ^ Pm) is Element of the carrier of n
Sum Pm is Element of the carrier of n
(Sum (Sum L)) + (Sum Pm) is Element of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the addF of n . ((Sum (Sum L)),(Sum Pm)) is Element of the carrier of n
<*(Sum Pm)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of n *
Sum <*(Sum Pm)*> is Element of the carrier of n
(Sum (Sum L)) + (Sum <*(Sum Pm)*>) is Element of the carrier of n
the addF of n . ((Sum (Sum L)),(Sum <*(Sum Pm)*>)) is Element of the carrier of n
(Sum L) ^ <*(Sum Pm)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum ((Sum L) ^ <*(Sum Pm)*>) is Element of the carrier of n
Sum <*Pm*> is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
(Sum L) ^ (Sum <*Pm*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum ((Sum L) ^ (Sum <*Pm*>)) is Element of the carrier of n
<*> ( the carrier of n *) is Relation-like non-empty empty-yielding NAT -defined the carrier of n * -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of ( the carrier of n *) *
( the carrier of n *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n *
FlattenSeq (<*> ( the carrier of n *)) is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of n *
Sum (FlattenSeq (<*> ( the carrier of n *))) is Element of the carrier of n
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of n *
Sum (<*> the carrier of n) is Element of the carrier of n
Sum (<*> ( the carrier of n *)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n
Sum (Sum (<*> ( the carrier of n *))) is Element of the carrier of n
n is non empty set
L is ZeroStr
the carrier of L is set
[:n, the carrier of L:] is Relation-like set
bool [:n, the carrier of L:] is non empty set
bool n is non empty set
Pm is Relation-like n -defined the carrier of L -valued Function-like quasi_total Element of bool [:n, the carrier of L:]
0. L is V82(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
x is Element of bool n
y is Element of n
Pm . y is Element of the carrier of L
z is Element of n
Pm . z is Element of the carrier of L
x is Element of bool n
y is Element of bool n
z is Element of n
Pm . z is Element of the carrier of L
n is non empty set
L is ZeroStr
the carrier of L is set
[:n, the carrier of L:] is Relation-like set
bool [: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 1-sorted
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
Pm . x is set
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
z . y 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 addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total 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 addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
(n,L,(n,L,Pm,x),y) is Element of the carrier of L
(n,L,Pm,y) is Element of the carrier of L
(n,L,x,y) is Element of the carrier of L
(n,L,Pm,y) + (n,L,x,y) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((n,L,Pm,y),(n,L,x,y)) is Element of the carrier of L
dom Pm is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
dom x is functional non empty Element of bool (Bags n)
Pm /. y is Element of the carrier of L
x /. y is Element of the carrier of L
dom (n,L,Pm,x) is functional non empty Element of bool (Bags n)
(dom Pm) /\ (dom x) is functional Element of bool (Bags n)
(n,L,Pm,x) /. y 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 addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
y . z is set
(n,L,Pm,x) . z is set
dom (n,L,Pm,x) is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
(n,L,Pm,x) /. z is Element of the carrier of L
(n,L,Pm,x) . z is Element of the carrier of L
(n,L,(n,L,Pm,x),z) is Element of the carrier of L
Pm /. z is Element of the carrier of L
Pm . z is Element of the carrier of L
(n,L,Pm,z) is Element of the carrier of L
x /. z is Element of the carrier of L
x . z is Element of the carrier of L
(n,L,x,z) is Element of the carrier of L
(n,L,y,z) is Element of the carrier of L
(n,L,Pm,z) + (n,L,x,z) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((n,L,Pm,z),(n,L,x,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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
- Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
(n,L,(- Pm),x) is Element of the carrier of L
(n,L,Pm,x) is Element of the carrier of L
- (n,L,Pm,x) is Element of the carrier of L
dom Pm is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
Pm /. x is Element of the carrier of L
dom (- Pm) is functional non empty Element of bool (Bags n)
(- Pm) /. 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 left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
- Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
x . y is set
(- Pm) . y is set
dom (- Pm) is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
(- Pm) /. y is Element of the carrier of L
(- Pm) . y is Element of the carrier of L
(n,L,(- Pm),y) is Element of the carrier of L
Pm /. y is Element of the carrier of L
Pm . y is Element of the carrier of L
(n,L,Pm,y) is Element of the carrier of L
(n,L,x,y) is Element of the carrier of L
- (n,L,Pm,y) 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
- Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
- (- Pm) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
dom Pm is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
dom (- Pm) is functional non empty Element of bool (Bags n)
dom (- (- Pm)) is functional non empty Element of bool (Bags n)
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,Pm,y) is Element of the carrier of L
Pm /. y is Element of the carrier of L
Pm . y is Element of the carrier of L
- (n,L,Pm,y) is Element of the carrier of L
- (- (n,L,Pm,y)) is Element of the carrier of L
(- Pm) /. y is Element of the carrier of L
(- Pm) . y is Element of the carrier of L
- ((- Pm) /. y) is Element of the carrier of L
(- (- Pm)) /. y is Element of the carrier of L
(- (- Pm)) . y is Element of the carrier of L
(n,L,(- (- Pm)),y) 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 right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
((Bags n),L,(n,L,Pm,x)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
((Bags n),L,Pm) is functional Element of bool (Bags n)
((Bags n),L,x) is functional Element of bool (Bags n)
((Bags n),L,Pm) \/ ((Bags n),L,x) is functional Element of bool (Bags n)
q is set
r is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,Pm,x),r) is Element of the carrier of L
0. L is V82(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(n,L,Pm,r) is Element of the carrier of L
(n,L,x,r) is Element of the carrier of L
(n,L,Pm,r) + (n,L,x,r) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((n,L,Pm,r),(n,L,x,r)) 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 Abelian right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,y,z) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y + z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,z,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z + y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,y,z),p) is Element of the carrier of L
(n,L,z,p) is Element of the carrier of L
(n,L,y,p) is Element of the carrier of L
(n,L,z,p) + (n,L,y,p) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((n,L,z,p),(n,L,y,p)) is Element of the carrier of L
(n,L,(n,L,z,y),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 add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,Pm,x),y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) + y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,x,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x + y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(n,L,x,y)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + (n,L,x,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,(n,L,Pm,x),y),z) is Element of the carrier of L
(n,L,(n,L,Pm,x),z) is Element of the carrier of L
(n,L,y,z) is Element of the carrier of L
(n,L,(n,L,Pm,x),z) + (n,L,y,z) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((n,L,(n,L,Pm,x),z),(n,L,y,z)) is Element of the carrier of L
(n,L,Pm,z) is Element of the carrier of L
(n,L,x,z) is Element of the carrier of L
(n,L,Pm,z) + (n,L,x,z) is Element of the carrier of L
the addF of L . ((n,L,Pm,z),(n,L,x,z)) is Element of the carrier of L
((n,L,Pm,z) + (n,L,x,z)) + (n,L,y,z) is Element of the carrier of L
the addF of L . (((n,L,Pm,z) + (n,L,x,z)),(n,L,y,z)) is Element of the carrier of L
(n,L,x,z) + (n,L,y,z) is Element of the carrier of L
the addF of L . ((n,L,x,z),(n,L,y,z)) is Element of the carrier of L
(n,L,Pm,z) + ((n,L,x,z) + (n,L,y,z)) is Element of the carrier of L
the addF of L . ((n,L,Pm,z),((n,L,x,z) + (n,L,y,z))) is Element of the carrier of L
(n,L,(n,L,x,y),z) is Element of the carrier of L
(n,L,Pm,z) + (n,L,(n,L,x,y),z) is Element of the carrier of L
the addF of L . ((n,L,Pm,z),(n,L,(n,L,x,y),z)) is Element of the carrier of L
(n,L,(n,L,Pm,(n,L,x,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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
- x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(- x)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + (- x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total 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
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. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
n is set
L is non empty ZeroStr
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total 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 Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
Pm is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
(n,L,(n,L),Pm) 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 right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(n,L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,x,z) is Element of the carrier of L
(n,L,Pm,z) is Element of the carrier of L
(n,L,(n,L),z) is Element of the carrier of L
(n,L,Pm,z) + (n,L,(n,L),z) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((n,L,Pm,z),(n,L,(n,L),z)) is Element of the carrier of L
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,y,z) is Element of the carrier of L
(n,L,y,z) + (0. L) is Element of the carrier of L
the addF of L . ((n,L,y,z),(0. 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
L is non empty right_unital multLoopStr_0
the carrier of L is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
1. L is Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total 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 left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,Pm) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
- Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(- Pm)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + (- Pm) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,x,z) is Element of the carrier of L
(n,L,Pm,z) is Element of the carrier of L
(n,L,(- Pm),z) is Element of the carrier of L
(n,L,Pm,z) + (n,L,(- Pm),z) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((n,L,Pm,z),(n,L,(- Pm),z)) is Element of the carrier of L
- (n,L,Pm,z) is Element of the carrier of L
(n,L,Pm,z) + (- (n,L,Pm,z)) is Element of the carrier of L
the addF of L . ((n,L,Pm,z),(- (n,L,Pm,z))) is Element of the carrier of L
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,y,z) is Element of the carrier of L
n is set
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() 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 right_unital multLoopStr_0
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like 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) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L),(EmptyBag n)) is Element of the carrier of L
dom (n,L) is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
x is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
(n,L,(n,L),x) is Element of the carrier of L
(n,L,(n,L),x) is Element of the carrier of L
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
decomp z is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
p is ordinal natural finite V38() V45() V46() ext-real set
len (decomp z) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
Seg (len (decomp z)) is non empty finite V40( len (decomp z)) V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (decomp z) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(decomp z) /. p is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
r is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*q,r*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
q + r is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
(n,L,Pm,q) is Element of the carrier of L
(n,L,x,r) is Element of the carrier of L
(n,L,Pm,q) * (n,L,x,r) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,Pm,q),(n,L,x,r)) is Element of the carrier of L
b19 is Element of the carrier of L
p is Element of the carrier of L
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
len p is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
Sum p is Element of the carrier of L
q is Element of the carrier of L
r is Element of the carrier of L
dom p is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
b19 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(decomp z) /. b19 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p /. b19 is Element of the carrier of L
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
(n,L,p,q) is Element of the carrier of L
decomp q is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp q) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
r is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,p,r) is Element of the carrier of L
b19 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum p is Element of the carrier of L
len p is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
decomp b19 is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp b19) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom p is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
r is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,p,r) is Element of the carrier of L
decomp r is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp r) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
b19 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum b19 is Element of the carrier of L
len b19 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom b19 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,q,r) is Element of the carrier of L
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum p is Element of the carrier of L
len p is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom p is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
q is ordinal natural finite V38() V45() V46() ext-real set
b19 /. q is Element of the carrier of L
b19 . q is set
p /. q is Element of the carrier of L
p . q is set
(decomp r) /. q is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
a1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
b1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*a1,b1*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,a1) is Element of the carrier of L
(n,L,x,b1) is Element of the carrier of L
(n,L,Pm,a1) * (n,L,x,b1) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,Pm,a1),(n,L,x,b1)) is Element of the carrier of L
O9 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*O9,O*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,O9) is Element of the carrier of L
(n,L,x,O) is Element of the carrier of L
(n,L,Pm,O9) * (n,L,x,O) is Element of the carrier of L
the multF of L . ((n,L,Pm,O9),(n,L,x,O)) is Element of the carrier of L
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like associative right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,x,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x + y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(n,L,x,y)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,Pm,x),(n,L,Pm,y)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) + (n,L,Pm,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,Pm,(n,L,x,y)),p) is Element of the carrier of L
decomp p is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
len (decomp p) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
q is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum q is Element of the carrier of L
len q is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom q is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(n,L,(n,L,Pm,y),p) is Element of the carrier of L
r is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum r is Element of the carrier of L
len r is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom r is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(n,L,(n,L,Pm,x),p) is Element of the carrier of L
b19 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum b19 is Element of the carrier of L
len b19 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom b19 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(len q) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
{ b₁ where b₁ is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L * : len b₁ = len q } is set
q is Relation-like NAT -defined the carrier of L -valued Function-like finite V40( len q) FinSequence-like FinSubsequence-like finite-support Element of (len q) -tuples_on the carrier of L
dom q is finite V40( len q) V62() V63() V64() V65() V66() V67() Element of bool NAT
p is Relation-like NAT -defined the carrier of L -valued Function-like finite V40( len q) FinSequence-like FinSubsequence-like finite-support Element of (len q) -tuples_on the carrier of L
dom p is finite V40( len q) V62() V63() V64() V65() V66() V67() Element of bool NAT
p + q is Relation-like NAT -defined the carrier of L -valued Function-like finite V40( len q) FinSequence-like FinSubsequence-like finite-support Element of (len q) -tuples_on the carrier of L
dom (p + q) is finite V40( len q) V62() V63() V64() V65() V66() V67() Element of bool NAT
a1 is ordinal natural finite V38() V45() V46() ext-real set
(decomp p) /. a1 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
q /. a1 is Element of the carrier of L
b1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
O9 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b1,O9*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,b1) is Element of the carrier of L
(n,L,(n,L,x,y),O9) is Element of the carrier of L
(n,L,Pm,b1) * (n,L,(n,L,x,y),O9) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,Pm,b1),(n,L,(n,L,x,y),O9)) is Element of the carrier of L
p /. a1 is Element of the carrier of L
p . a1 is set
q /. a1 is Element of the carrier of L
q . a1 is set
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*O,O*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,O) is Element of the carrier of L
(n,L,y,O) is Element of the carrier of L
(n,L,Pm,O) * (n,L,y,O) is Element of the carrier of L
the multF of L . ((n,L,Pm,O),(n,L,y,O)) is Element of the carrier of L
R is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
x is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*R,x*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,R) is Element of the carrier of L
(n,L,x,x) is Element of the carrier of L
(n,L,Pm,R) * (n,L,x,x) is Element of the carrier of L
the multF of L . ((n,L,Pm,R),(n,L,x,x)) is Element of the carrier of L
q . a1 is set
(n,L,x,O9) is Element of the carrier of L
(n,L,y,O9) is Element of the carrier of L
(n,L,x,O9) + (n,L,y,O9) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the addF of L . ((n,L,x,O9),(n,L,y,O9)) is Element of the carrier of L
(n,L,Pm,b1) * ((n,L,x,O9) + (n,L,y,O9)) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),((n,L,x,O9) + (n,L,y,O9))) is Element of the carrier of L
(n,L,Pm,b1) * (n,L,x,O9) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),(n,L,x,O9)) is Element of the carrier of L
(n,L,Pm,b1) * (n,L,y,O9) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),(n,L,y,O9)) is Element of the carrier of L
((n,L,Pm,b1) * (n,L,x,O9)) + ((n,L,Pm,b1) * (n,L,y,O9)) is Element of the carrier of L
the addF of L . (((n,L,Pm,b1) * (n,L,x,O9)),((n,L,Pm,b1) * (n,L,y,O9))) is Element of the carrier of L
(p + q) . a1 is set
len (p + q) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
Sum p is Element of the carrier of L
Sum q is Element of the carrier of L
(Sum p) + (Sum q) is Element of the carrier of L
the addF of L . ((Sum p),(Sum q)) is Element of the carrier of L
(n,L,(n,L,(n,L,Pm,x),(n,L,Pm,y)),p) is Element of the carrier of L
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like associative right-distributive left-distributive right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,Pm,x),y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,x,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(n,L,x,y)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
decomp p is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
len (decomp p) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
a1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len a1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom a1 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
rng a1 is finite set
3 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 3 } is set
(3 -tuples_on (Bags n)) * is functional non empty FinSequence-membered FinSequenceSet of 3 -tuples_on (Bags n)
b1 is set
O9 is set
a1 . O9 is set
(decomp p) /. O9 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
((decomp p) /. O9) /. 2 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
((decomp p) /. O9) /. 1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
decomp (((decomp p) /. O9) /. 1) is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp (((decomp p) /. O9) /. 1)) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
<*(((decomp p) /. O9) /. 2)*> is Relation-like NAT -defined Bags n -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*> is Relation-like NAT -defined (Bags n) * -valued Function-like Function-yielding V25() finite V40( len (decomp (((decomp p) /. O9) /. 1))) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (len (decomp (((decomp p) /. O9) /. 1))) -tuples_on ((Bags n) *)
(len (decomp (((decomp p) /. O9) /. 1))) -tuples_on ((Bags n) *) is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
((Bags n) *) * is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
{ b₁ where b₁ is Relation-like NAT -defined (Bags n) * -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((Bags n) *) * : len b₁ = len (decomp (((decomp p) /. O9) /. 1)) } is set
Seg (len (decomp (((decomp p) /. O9) /. 1))) is non empty finite V40( len (decomp (((decomp p) /. O9) /. 1))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(Seg (len (decomp (((decomp p) /. O9) /. 1)))) --> <*(((decomp p) /. O9) /. 2)*> is Relation-like non-empty Seg (len (decomp (((decomp p) /. O9) /. 1))) -defined Seg (len (decomp (((decomp p) /. O9) /. 1))) -defined (Bags n) * -valued {<*(((decomp p) /. O9) /. 2)*>} -valued Function-like constant non empty total total quasi_total Function-yielding V25() finite FinSequence-like FinSubsequence-like finite-support Element of bool [:(Seg (len (decomp (((decomp p) /. O9) /. 1)))),{<*(((decomp p) /. O9) /. 2)*>}:]
{<*(((decomp p) /. O9) /. 2)*>} is functional non empty trivial finite V37() V40(1) set
[:(Seg (len (decomp (((decomp p) /. O9) /. 1)))),{<*(((decomp p) /. O9) /. 2)*>}:] is Relation-like non empty finite set
bool [:(Seg (len (decomp (((decomp p) /. O9) /. 1)))),{<*(((decomp p) /. O9) /. 2)*>}:] is non empty finite V37() set
(decomp (((decomp p) /. O9) /. 1)) ^^ ((len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*>) is Relation-like NAT -defined Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
dom ((decomp (((decomp p) /. O9) /. 1)) ^^ ((len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*>)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (decomp (((decomp p) /. O9) /. 1)) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom ((len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*>) is finite V40( len (decomp (((decomp p) /. O9) /. 1))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. O9) /. 1))) /\ (dom ((len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*>)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. O9) /. 1))) /\ (Seg (len (decomp (((decomp p) /. O9) /. 1)))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. O9) /. 1))) /\ (dom (decomp (((decomp p) /. O9) /. 1))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
rng ((decomp (((decomp p) /. O9) /. 1)) ^^ ((len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*>)) is finite set
1 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 1 } is set
p is set
q is set
((decomp (((decomp p) /. O9) /. 1)) ^^ ((len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*>)) . q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp (((decomp p) /. O9) /. 1)) . q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng (decomp (((decomp p) /. O9) /. 1)) is functional non empty finite FinSequence-membered Element of bool (2 -tuples_on (Bags n))
bool (2 -tuples_on (Bags n)) is non empty set
vdbr is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
((len (decomp (((decomp p) /. O9) /. 1))) |-> <*(((decomp p) /. O9) /. 2)*>) . vdbr is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
vdbl is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
y is Relation-like NAT -defined Bags n -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of 1 -tuples_on (Bags n)
vdbl ^ y is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(2 + 1) FinSequence-like FinSubsequence-like finite-support FinSequence of Bags n
2 + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
R is ordinal natural finite V38() V45() V46() ext-real set
a1 . R is set
[:(3 -tuples_on (Bags n)), the carrier of L:] is Relation-like non empty set
bool [:(3 -tuples_on (Bags n)), the carrier of L:] is non empty set
b1 is Relation-like 3 -tuples_on (Bags n) -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(3 -tuples_on (Bags n)), the carrier of L:]
O9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len O9 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom O9 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
rng O9 is finite set
O is set
O is set
O9 . O is set
R is ordinal natural finite V38() V45() V46() ext-real set
(decomp p) /. R is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
((decomp p) /. R) /. 2 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
decomp (((decomp p) /. R) /. 2) is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
((decomp p) /. R) /. 1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
len (decomp (((decomp p) /. R) /. 2)) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
<*(((decomp p) /. R) /. 1)*> is Relation-like NAT -defined Bags n -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*> is Relation-like NAT -defined (Bags n) * -valued Function-like Function-yielding V25() finite V40( len (decomp (((decomp p) /. R) /. 2))) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (len (decomp (((decomp p) /. R) /. 2))) -tuples_on ((Bags n) *)
(len (decomp (((decomp p) /. R) /. 2))) -tuples_on ((Bags n) *) is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
((Bags n) *) * is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
{ b₁ where b₁ is Relation-like NAT -defined (Bags n) * -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((Bags n) *) * : len b₁ = len (decomp (((decomp p) /. R) /. 2)) } is set
Seg (len (decomp (((decomp p) /. R) /. 2))) is non empty finite V40( len (decomp (((decomp p) /. R) /. 2))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(Seg (len (decomp (((decomp p) /. R) /. 2)))) --> <*(((decomp p) /. R) /. 1)*> is Relation-like non-empty Seg (len (decomp (((decomp p) /. R) /. 2))) -defined Seg (len (decomp (((decomp p) /. R) /. 2))) -defined (Bags n) * -valued {<*(((decomp p) /. R) /. 1)*>} -valued Function-like constant non empty total total quasi_total Function-yielding V25() finite FinSequence-like FinSubsequence-like finite-support Element of bool [:(Seg (len (decomp (((decomp p) /. R) /. 2)))),{<*(((decomp p) /. R) /. 1)*>}:]
{<*(((decomp p) /. R) /. 1)*>} is functional non empty trivial finite V37() V40(1) set
[:(Seg (len (decomp (((decomp p) /. R) /. 2)))),{<*(((decomp p) /. R) /. 1)*>}:] is Relation-like non empty finite set
bool [:(Seg (len (decomp (((decomp p) /. R) /. 2)))),{<*(((decomp p) /. R) /. 1)*>}:] is non empty finite V37() set
((len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*>) ^^ (decomp (((decomp p) /. R) /. 2)) is Relation-like NAT -defined Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
dom (((len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*>) ^^ (decomp (((decomp p) /. R) /. 2))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (decomp (((decomp p) /. R) /. 2)) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom ((len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*>) is finite V40( len (decomp (((decomp p) /. R) /. 2))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. R) /. 2))) /\ (dom ((len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*>)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. R) /. 2))) /\ (Seg (len (decomp (((decomp p) /. R) /. 2)))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. R) /. 2))) /\ (dom (decomp (((decomp p) /. R) /. 2))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
rng (((len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*>) ^^ (decomp (((decomp p) /. R) /. 2))) is finite set
1 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 1 } is set
vdbl is set
vdbr is set
(((len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*>) ^^ (decomp (((decomp p) /. R) /. 2))) . vdbr is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp (((decomp p) /. R) /. 2)) . vdbr is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng (decomp (((decomp p) /. R) /. 2)) is functional non empty finite FinSequence-membered Element of bool (2 -tuples_on (Bags n))
bool (2 -tuples_on (Bags n)) is non empty set
P is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
((len (decomp (((decomp p) /. R) /. 2))) |-> <*(((decomp p) /. R) /. 1)*>) . P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
q is Relation-like NAT -defined Bags n -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of 1 -tuples_on (Bags n)
rs is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
q ^ rs is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(1 + 2) FinSequence-like FinSubsequence-like finite-support FinSequence of Bags n
1 + 2 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
O9 . R is set
O is Relation-like NAT -defined (3 -tuples_on (Bags n)) * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (3 -tuples_on (Bags n)) *
FlattenSeq O is Relation-like NAT -defined 3 -tuples_on (Bags n) -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (3 -tuples_on (Bags n)) *
O is Relation-like NAT -defined (3 -tuples_on (Bags n)) * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (3 -tuples_on (Bags n)) *
FlattenSeq O is Relation-like NAT -defined 3 -tuples_on (Bags n) -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (3 -tuples_on (Bags n)) *
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,p,p) is Element of the carrier of L
y is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum y is Element of the carrier of L
len y is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom y is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom O is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (decomp p) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
b1 * (FlattenSeq O) is Relation-like NAT -defined the carrier of L -valued Function-like finite finite-support Element of bool [:NAT, the carrier of L:]
[:NAT, the carrier of L:] is Relation-like non trivial non finite set
bool [:NAT, the carrier of L:] is non empty non trivial non finite set
b1 * (FlattenSeq O) is Relation-like NAT -defined the carrier of L -valued Function-like finite finite-support Element of bool [:NAT, the carrier of L:]
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
dom O is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom O) --> b1 is Relation-like non-empty dom O -defined bool [:(3 -tuples_on (Bags n)), the carrier of L:] -valued Function-like constant total quasi_total Function-yielding V25() finite finite-support Element of bool [:(dom O),(bool [:(3 -tuples_on (Bags n)), the carrier of L:]):]
[:(dom O),(bool [:(3 -tuples_on (Bags n)), the carrier of L:]):] is Relation-like set
bool [:(dom O),(bool [:(3 -tuples_on (Bags n)), the carrier of L:]):] is non empty set
{b1} is functional non empty trivial finite V40(1) set
[:(dom O),{b1}:] is Relation-like finite set
((dom O) --> b1) ** O is Relation-like Function-like set
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
vdbl is Relation-like NAT -defined the carrier of L * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of L *
FlattenSeq vdbl is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
dom b1 is functional non empty FinSequence-membered Element of bool (3 -tuples_on (Bags n))
bool (3 -tuples_on (Bags n)) is non empty set
Sum vdbl is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
dom vdbl is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom ((dom O) --> b1) is finite V62() V63() V64() V65() V66() V67() Element of bool (dom O)
bool (dom O) is non empty finite V37() set
(dom ((dom O) --> b1)) /\ (dom O) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom O) /\ (dom O) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (Sum vdbl) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len (Sum vdbl) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
rs is ordinal natural finite V38() V45() V46() ext-real set
(Sum vdbl) /. rs is Element of the carrier of L
(Sum vdbl) . rs is set
y /. rs is Element of the carrier of L
y . rs is set
(decomp p) /. rs is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
P is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
P is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*P,P*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,(n,L,Pm,x),P) is Element of the carrier of L
(n,L,y,P) is Element of the carrier of L
(n,L,(n,L,Pm,x),P) * (n,L,y,P) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,(n,L,Pm,x),P),(n,L,y,P)) is Element of the carrier of L
len <*P,P*> is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom <*P,P*> is non empty finite V40(2) V62() V63() V64() V65() V66() V67() Element of bool NAT
((decomp p) /. rs) /. 1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
<*P,P*> . 1 is set
O . rs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
((decomp p) /. rs) /. 2 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
decomp (((decomp p) /. rs) /. 1) is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp (((decomp p) /. rs) /. 1)) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
<*(((decomp p) /. rs) /. 2)*> is Relation-like NAT -defined Bags n -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(len (decomp (((decomp p) /. rs) /. 1))) |-> <*(((decomp p) /. rs) /. 2)*> is Relation-like NAT -defined (Bags n) * -valued Function-like Function-yielding V25() finite V40( len (decomp (((decomp p) /. rs) /. 1))) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (len (decomp (((decomp p) /. rs) /. 1))) -tuples_on ((Bags n) *)
(len (decomp (((decomp p) /. rs) /. 1))) -tuples_on ((Bags n) *) is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
((Bags n) *) * is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
{ b₁ where b₁ is Relation-like NAT -defined (Bags n) * -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((Bags n) *) * : len b₁ = len (decomp (((decomp p) /. rs) /. 1)) } is set
Seg (len (decomp (((decomp p) /. rs) /. 1))) is non empty finite V40( len (decomp (((decomp p) /. rs) /. 1))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(Seg (len (decomp (((decomp p) /. rs) /. 1)))) --> <*(((decomp p) /. rs) /. 2)*> is Relation-like non-empty Seg (len (decomp (((decomp p) /. rs) /. 1))) -defined Seg (len (decomp (((decomp p) /. rs) /. 1))) -defined (Bags n) * -valued {<*(((decomp p) /. rs) /. 2)*>} -valued Function-like constant non empty total total quasi_total Function-yielding V25() finite FinSequence-like FinSubsequence-like finite-support Element of bool [:(Seg (len (decomp (((decomp p) /. rs) /. 1)))),{<*(((decomp p) /. rs) /. 2)*>}:]
{<*(((decomp p) /. rs) /. 2)*>} is functional non empty trivial finite V37() V40(1) set
[:(Seg (len (decomp (((decomp p) /. rs) /. 1)))),{<*(((decomp p) /. rs) /. 2)*>}:] is Relation-like non empty finite set
bool [:(Seg (len (decomp (((decomp p) /. rs) /. 1)))),{<*(((decomp p) /. rs) /. 2)*>}:] is non empty finite V37() set
(decomp (((decomp p) /. rs) /. 1)) ^^ ((len (decomp (((decomp p) /. rs) /. 1))) |-> <*(((decomp p) /. rs) /. 2)*>) is Relation-like NAT -defined Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
dom (O . rs) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (decomp (((decomp p) /. rs) /. 1)) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom ((len (decomp (((decomp p) /. rs) /. 1))) |-> <*(((decomp p) /. rs) /. 2)*>) is finite V40( len (decomp (((decomp p) /. rs) /. 1))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. rs) /. 1))) /\ (dom ((len (decomp (((decomp p) /. rs) /. 1))) |-> <*(((decomp p) /. rs) /. 2)*>)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. rs) /. 1))) /\ (Seg (len (decomp (((decomp p) /. rs) /. 1)))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. rs) /. 1))) /\ (dom (decomp (((decomp p) /. rs) /. 1))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(O . rs) * b1 is Relation-like NAT -defined the carrier of L -valued Function-like finite finite-support set
rng O is functional finite FinSequence-membered Element of bool ((3 -tuples_on (Bags n)) *)
bool ((3 -tuples_on (Bags n)) *) is non empty set
dbrk is Relation-like NAT -defined 3 -tuples_on (Bags n) -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 3 -tuples_on (Bags n)
rng dbrk is functional finite FinSequence-membered Element of bool (3 -tuples_on (Bags n))
dom ((O . rs) * b1) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom dbrk is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
decomp P is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp P) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
b2 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum b2 is Element of the carrier of L
len b2 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom b2 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(L,b2,(n,L,y,P)) is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
dom (L,b2,(n,L,y,P)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
<*P,P*> . 2 is set
Sum (L,b2,(n,L,y,P)) is Element of the carrier of L
(Sum b2) * (n,L,y,P) is Element of the carrier of L
the multF of L . ((Sum b2),(n,L,y,P)) is Element of the carrier of L
b19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len b19 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len (L,b2,(n,L,y,P)) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom b19 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
qrs is ordinal natural finite V38() V45() V46() ext-real set
(decomp P) /. qrs is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
b2 /. qrs is Element of the carrier of L
i is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
i9 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*i,i9*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,i) is Element of the carrier of L
(n,L,x,i9) is Element of the carrier of L
(n,L,Pm,i) * (n,L,x,i9) is Element of the carrier of L
the multF of L . ((n,L,Pm,i),(n,L,x,i9)) is Element of the carrier of L
vdbrk is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
((len (decomp (((decomp p) /. rs) /. 1))) |-> <*(((decomp p) /. rs) /. 2)*>) . vdbrk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp P) . qrs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dbrk . qrs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
<*P*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support set
<*i,i9*> ^ <*P*> is Relation-like NAT -defined Function-like non empty finite V40(2 + 1) FinSequence-like FinSubsequence-like finite-support set
2 + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
<*i,i9,P*> is Relation-like NAT -defined Function-like non empty finite V40(3) FinSequence-like FinSubsequence-like finite-support set
b11 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
b12 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
b1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
<*b11,b12,b1*> is Relation-like NAT -defined Function-like non empty finite V40(3) FinSequence-like FinSubsequence-like finite-support set
((O . rs) * b1) . qrs is set
b1 . (dbrk . qrs) is set
b119 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(3) FinSequence-like FinSubsequence-like finite-support Element of 3 -tuples_on (Bags n)
b119 /. 1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,Pm,(b119 /. 1)) is Element of the carrier of L
b119 /. 2 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,x,(b119 /. 2)) is Element of the carrier of L
(n,L,Pm,(b119 /. 1)) * (n,L,x,(b119 /. 2)) is Element of the carrier of L
the multF of L . ((n,L,Pm,(b119 /. 1)),(n,L,x,(b119 /. 2))) is Element of the carrier of L
b119 /. 3 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,y,(b119 /. 3)) is Element of the carrier of L
((n,L,Pm,(b119 /. 1)) * (n,L,x,(b119 /. 2))) * (n,L,y,(b119 /. 3)) is Element of the carrier of L
the multF of L . (((n,L,Pm,(b119 /. 1)) * (n,L,x,(b119 /. 2))),(n,L,y,(b119 /. 3))) is Element of the carrier of L
(n,L,Pm,b11) is Element of the carrier of L
(n,L,Pm,b11) * (n,L,x,(b119 /. 2)) is Element of the carrier of L
the multF of L . ((n,L,Pm,b11),(n,L,x,(b119 /. 2))) is Element of the carrier of L
((n,L,Pm,b11) * (n,L,x,(b119 /. 2))) * (n,L,y,(b119 /. 3)) is Element of the carrier of L
the multF of L . (((n,L,Pm,b11) * (n,L,x,(b119 /. 2))),(n,L,y,(b119 /. 3))) is Element of the carrier of L
((n,L,Pm,i) * (n,L,x,i9)) * (n,L,y,(b119 /. 3)) is Element of the carrier of L
the multF of L . (((n,L,Pm,i) * (n,L,x,i9)),(n,L,y,(b119 /. 3))) is Element of the carrier of L
(b2 /. qrs) * (n,L,y,P) is Element of the carrier of L
the multF of L . ((b2 /. qrs),(n,L,y,P)) is Element of the carrier of L
(L,b2,(n,L,y,P)) /. qrs is Element of the carrier of L
(L,b2,(n,L,y,P)) . qrs is set
vdbl /. rs is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
vdbl . rs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
((dom O) --> b1) . rs is Relation-like Function-like set
(O . rs) * (((dom O) --> b1) . rs) is Relation-like NAT -defined Function-like finite finite-support set
(dom O) --> b1 is Relation-like non-empty dom O -defined bool [:(3 -tuples_on (Bags n)), the carrier of L:] -valued Function-like constant total quasi_total Function-yielding V25() finite finite-support Element of bool [:(dom O),(bool [:(3 -tuples_on (Bags n)), the carrier of L:]):]
[:(dom O),(bool [:(3 -tuples_on (Bags n)), the carrier of L:]):] is Relation-like set
bool [:(dom O),(bool [:(3 -tuples_on (Bags n)), the carrier of L:]):] is non empty set
[:(dom O),{b1}:] is Relation-like finite set
((dom O) --> b1) ** O is Relation-like Function-like set
q is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
vdbr is Relation-like NAT -defined the carrier of L * -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of L *
FlattenSeq vdbr is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
Sum q is Element of the carrier of L
Sum vdbr is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum (Sum vdbr) is Element of the carrier of L
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,q,p) is Element of the carrier of L
rs is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum rs is Element of the carrier of L
len rs is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom rs is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom vdbr is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom ((dom O) --> b1) is finite V62() V63() V64() V65() V66() V67() Element of bool (dom O)
bool (dom O) is non empty finite V37() set
(dom ((dom O) --> b1)) /\ (dom O) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom O) /\ (dom O) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (Sum vdbr) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len (Sum vdbr) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
P is ordinal natural finite V38() V45() V46() ext-real set
(Sum vdbr) /. P is Element of the carrier of L
(Sum vdbr) . P is set
O . P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp p) /. P is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
((decomp p) /. P) /. 1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
((decomp p) /. P) /. 2 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
decomp (((decomp p) /. P) /. 2) is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp (((decomp p) /. P) /. 2)) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
<*(((decomp p) /. P) /. 1)*> is Relation-like NAT -defined Bags n -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(len (decomp (((decomp p) /. P) /. 2))) |-> <*(((decomp p) /. P) /. 1)*> is Relation-like NAT -defined (Bags n) * -valued Function-like Function-yielding V25() finite V40( len (decomp (((decomp p) /. P) /. 2))) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (len (decomp (((decomp p) /. P) /. 2))) -tuples_on ((Bags n) *)
(len (decomp (((decomp p) /. P) /. 2))) -tuples_on ((Bags n) *) is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
{ b₁ where b₁ is Relation-like NAT -defined (Bags n) * -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((Bags n) *) * : len b₁ = len (decomp (((decomp p) /. P) /. 2)) } is set
Seg (len (decomp (((decomp p) /. P) /. 2))) is non empty finite V40( len (decomp (((decomp p) /. P) /. 2))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(Seg (len (decomp (((decomp p) /. P) /. 2)))) --> <*(((decomp p) /. P) /. 1)*> is Relation-like non-empty Seg (len (decomp (((decomp p) /. P) /. 2))) -defined Seg (len (decomp (((decomp p) /. P) /. 2))) -defined (Bags n) * -valued {<*(((decomp p) /. P) /. 1)*>} -valued Function-like constant non empty total total quasi_total Function-yielding V25() finite FinSequence-like FinSubsequence-like finite-support Element of bool [:(Seg (len (decomp (((decomp p) /. P) /. 2)))),{<*(((decomp p) /. P) /. 1)*>}:]
{<*(((decomp p) /. P) /. 1)*>} is functional non empty trivial finite V37() V40(1) set
[:(Seg (len (decomp (((decomp p) /. P) /. 2)))),{<*(((decomp p) /. P) /. 1)*>}:] is Relation-like non empty finite set
bool [:(Seg (len (decomp (((decomp p) /. P) /. 2)))),{<*(((decomp p) /. P) /. 1)*>}:] is non empty finite V37() set
((len (decomp (((decomp p) /. P) /. 2))) |-> <*(((decomp p) /. P) /. 1)*>) ^^ (decomp (((decomp p) /. P) /. 2)) is Relation-like NAT -defined Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
dom (O . P) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (decomp (((decomp p) /. P) /. 2)) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom ((len (decomp (((decomp p) /. P) /. 2))) |-> <*(((decomp p) /. P) /. 1)*>) is finite V40( len (decomp (((decomp p) /. P) /. 2))) V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. P) /. 2))) /\ (dom ((len (decomp (((decomp p) /. P) /. 2))) |-> <*(((decomp p) /. P) /. 1)*>)) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. P) /. 2))) /\ (Seg (len (decomp (((decomp p) /. P) /. 2)))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(dom (decomp (((decomp p) /. P) /. 2))) /\ (dom (decomp (((decomp p) /. P) /. 2))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
rng O is functional finite FinSequence-membered Element of bool ((3 -tuples_on (Bags n)) *)
(O . P) * b1 is Relation-like NAT -defined the carrier of L -valued Function-like finite finite-support set
dbrk is Relation-like NAT -defined 3 -tuples_on (Bags n) -valued Function-like Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 3 -tuples_on (Bags n)
rng dbrk is functional finite FinSequence-membered Element of bool (3 -tuples_on (Bags n))
dom ((O . P) * b1) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom dbrk is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
rs /. P is Element of the carrier of L
rs . P is set
b1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
b2 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b1,b2*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,b1) is Element of the carrier of L
(n,L,(n,L,x,y),b2) is Element of the carrier of L
(n,L,Pm,b1) * (n,L,(n,L,x,y),b2) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),(n,L,(n,L,x,y),b2)) is Element of the carrier of L
decomp b2 is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
len (decomp b2) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
qrs is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum qrs is Element of the carrier of L
len qrs is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom qrs is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
(n,L,Pm,b1) * qrs is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
dom ((n,L,Pm,b1) * qrs) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
len ((n,L,Pm,b1) * qrs) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len <*b1,b2*> is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom <*b1,b2*> is non empty finite V40(2) V62() V63() V64() V65() V66() V67() Element of bool NAT
<*b1,b2*> . 1 is set
Sum ((n,L,Pm,b1) * qrs) is Element of the carrier of L
(n,L,Pm,b1) * (Sum qrs) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),(Sum qrs)) is Element of the carrier of L
<*b1,b2*> . 2 is set
vdbrk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom vdbrk is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
i is ordinal natural finite V38() V45() V46() ext-real set
(decomp b2) /. i is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
qrs /. i is Element of the carrier of L
b11 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
b12 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b11,b12*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,x,b11) is Element of the carrier of L
(n,L,y,b12) is Element of the carrier of L
(n,L,x,b11) * (n,L,y,b12) is Element of the carrier of L
the multF of L . ((n,L,x,b11),(n,L,y,b12)) is Element of the carrier of L
i9 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
((len (decomp (((decomp p) /. P) /. 2))) |-> <*(((decomp p) /. P) /. 1)*>) . i9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp b2) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dbrk . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
<*b1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support set
<*b1*> ^ <*b11,b12*> is Relation-like NAT -defined Function-like non empty finite V40(1 + 2) FinSequence-like FinSubsequence-like finite-support set
1 + 2 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
<*b1,b11,b12*> is Relation-like NAT -defined Function-like non empty finite V40(3) FinSequence-like FinSubsequence-like finite-support set
b19 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
b119 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
b129 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
<*b19,b119,b129*> is Relation-like NAT -defined Function-like non empty finite V40(3) FinSequence-like FinSubsequence-like finite-support set
((O . P) * b1) . i is set
b1 . (dbrk . i) is set
B is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(3) FinSequence-like FinSubsequence-like finite-support Element of 3 -tuples_on (Bags n)
B /. 1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,Pm,(B /. 1)) is Element of the carrier of L
B /. 2 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,x,(B /. 2)) is Element of the carrier of L
(n,L,Pm,(B /. 1)) * (n,L,x,(B /. 2)) is Element of the carrier of L
the multF of L . ((n,L,Pm,(B /. 1)),(n,L,x,(B /. 2))) is Element of the carrier of L
B /. 3 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,y,(B /. 3)) is Element of the carrier of L
((n,L,Pm,(B /. 1)) * (n,L,x,(B /. 2))) * (n,L,y,(B /. 3)) is Element of the carrier of L
the multF of L . (((n,L,Pm,(B /. 1)) * (n,L,x,(B /. 2))),(n,L,y,(B /. 3))) is Element of the carrier of L
(n,L,Pm,b1) * (n,L,x,(B /. 2)) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),(n,L,x,(B /. 2))) is Element of the carrier of L
((n,L,Pm,b1) * (n,L,x,(B /. 2))) * (n,L,y,(B /. 3)) is Element of the carrier of L
the multF of L . (((n,L,Pm,b1) * (n,L,x,(B /. 2))),(n,L,y,(B /. 3))) is Element of the carrier of L
(n,L,Pm,b1) * (n,L,x,b11) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),(n,L,x,b11)) is Element of the carrier of L
((n,L,Pm,b1) * (n,L,x,b11)) * (n,L,y,(B /. 3)) is Element of the carrier of L
the multF of L . (((n,L,Pm,b1) * (n,L,x,b11)),(n,L,y,(B /. 3))) is Element of the carrier of L
((n,L,Pm,b1) * (n,L,x,b11)) * (n,L,y,b12) is Element of the carrier of L
the multF of L . (((n,L,Pm,b1) * (n,L,x,b11)),(n,L,y,b12)) is Element of the carrier of L
(n,L,Pm,b1) * (qrs /. i) is Element of the carrier of L
the multF of L . ((n,L,Pm,b1),(qrs /. i)) is Element of the carrier of L
((n,L,Pm,b1) * qrs) /. i is Element of the carrier of L
((n,L,Pm,b1) * qrs) . i is set
len vdbrk is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
vdbr /. P is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
vdbr . P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
((dom O) --> b1) . P is Relation-like Function-like set
(O . P) * (((dom O) --> b1) . P) is Relation-like NAT -defined Function-like finite finite-support set
dom (FlattenSeq O) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
[:(dom (FlattenSeq O)),(dom (FlattenSeq O)):] is Relation-like RAT -valued INT -valued finite V52() V53() V54() V55() set
bool [:(dom (FlattenSeq O)),(dom (FlattenSeq O)):] is non empty finite V37() set
P is Relation-like dom (FlattenSeq O) -defined dom (FlattenSeq O) -valued Function-like one-to-one total quasi_total onto bijective finite V52() V53() V54() V55() finite-support Element of bool [:(dom (FlattenSeq O)),(dom (FlattenSeq O)):]
(FlattenSeq O) * P is Relation-like dom (FlattenSeq O) -defined 3 -tuples_on (Bags n) -valued Function-like Function-yielding V25() finite finite-support Element of bool [:(dom (FlattenSeq O)),(3 -tuples_on (Bags n)):]
[:(dom (FlattenSeq O)),(3 -tuples_on (Bags n)):] is Relation-like set
bool [:(dom (FlattenSeq O)),(3 -tuples_on (Bags n)):] is non empty set
rng (FlattenSeq O) is functional finite FinSequence-membered Element of bool (3 -tuples_on (Bags n))
dom p is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
[:(dom p),(dom p):] is Relation-like RAT -valued INT -valued finite V52() V53() V54() V55() set
bool [:(dom p),(dom p):] is non empty finite V37() set
P is Relation-like dom p -defined dom p -valued Function-like one-to-one total quasi_total onto bijective finite V52() V53() V54() V55() finite-support Element of bool [:(dom p),(dom p):]
p * P is Relation-like dom p -defined the carrier of L -valued Function-like finite finite-support Element of bool [:(dom p), the carrier of L:]
[:(dom p), the carrier of L:] is Relation-like set
bool [:(dom p), the carrier of L:] is non empty set
Sum p is Element of the carrier of L
Sum (Sum vdbl) is Element of the carrier of L
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like commutative Abelian add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,y,z) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,z,y) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
r is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
decomp r is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,p,r) is Element of the carrier of L
len (decomp r) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
b19 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum b19 is Element of the carrier of L
len b19 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom b19 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
dom (decomp r) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
q is set
p is non empty set
(decomp r) /. q is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
a1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
b1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*a1,b1*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
a1 + b1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b1,a1*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
O9 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(decomp r) /. O9 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
O is set
O is set
(decomp r) . q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp r) . O is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
[:p,p:] is Relation-like non empty set
bool [:p,p:] is non empty set
q is Relation-like p -defined p -valued Function-like non empty total quasi_total Element of bool [:p,p:]
dom q is non empty Element of bool p
bool p is non empty set
rng q is non empty Element of bool p
a1 is set
(decomp r) . a1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
q . a1 is set
(decomp r) . (q . a1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
b1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
O9 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b1,O9*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
<*O9,b1*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
q . (q . a1) is set
(decomp r) . (q . (q . a1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*O,O*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
<*O,O*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
a1 is set
dom q is non empty set
b1 is set
q . a1 is set
q . b1 is set
(decomp r) . b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp r) . (q . b1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
O9 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*O9,O*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
<*O,O9*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(decomp r) . a1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp r) . (q . a1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
R is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*O,R*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
<*R,O*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
[:(dom b19),(dom b19):] is Relation-like RAT -valued INT -valued finite V52() V53() V54() V55() set
bool [:(dom b19),(dom b19):] is non empty finite V37() set
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,q,r) is Element of the carrier of L
b1 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum b1 is Element of the carrier of L
len b1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom b1 is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
a1 is Relation-like dom b19 -defined dom b19 -valued Function-like one-to-one total quasi_total onto bijective finite V52() V53() V54() V55() finite-support Element of bool [:(dom b19),(dom b19):]
O9 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
a1 . O9 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(decomp r) /. O9 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
b1 /. O9 is Element of the carrier of L
O is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
R is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*O,R*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,z,O) is Element of the carrier of L
(n,L,y,R) is Element of the carrier of L
(n,L,z,O) * (n,L,y,R) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,z,O),(n,L,y,R)) is Element of the carrier of L
b1 . O9 is set
(decomp r) . O9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp r) . (a1 . O9) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
x is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*x,y*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
<*y,x*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
rng a1 is finite V62() V63() V64() V65() V66() V67() Element of bool (dom b19)
bool (dom b19) is non empty finite V37() set
O is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
b19 /. O is Element of the carrier of L
b19 . O is set
(decomp r) /. O is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*p,q*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,y,p) is Element of the carrier of L
(n,L,z,q) is Element of the carrier of L
(n,L,y,p) * (n,L,z,q) is Element of the carrier of L
the multF of L . ((n,L,y,p),(n,L,z,q)) is Element of the carrier of L
(decomp r) . O is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
b19 . (a1 . O9) is set
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(n,L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,Pm,(n,L)),y) is Element of the carrier of L
decomp y is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
len (decomp y) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
z is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum z is Element of the carrier of L
len z is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom z is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
p is ordinal natural finite V38() V45() V46() ext-real set
(decomp y) /. p is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
z /. p is Element of the carrier of L
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
r is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*q,r*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,q) is Element of the carrier of L
(n,L,(n,L),r) is Element of the carrier of L
(n,L,Pm,q) * (n,L,(n,L),r) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,Pm,q),(n,L,(n,L),r)) is Element of the carrier of L
(n,L,Pm,q) * (0. L) is Element of the carrier of L
the multF of L . ((n,L,Pm,q),(0. L)) is Element of the carrier of L
(n,L,(n,L),y) is Element of the carrier of L
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
1. L is V82(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(n,L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,Pm,(n,L)),z) is Element of the carrier of L
decomp z is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
len (decomp z) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum p is Element of the carrier of L
len p is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom p is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
q is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
r is Element of the carrier of L
<*r*> is Relation-like NAT -defined the carrier of L -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
q ^ <*r*> is Relation-like NAT -defined the carrier of L -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
<*> the carrier of L is Relation-like non-empty empty-yielding NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of L *
Sum q is Element of the carrier of L
<*> the carrier of L is Relation-like non-empty empty-yielding NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of L *
len q is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len <*r*> is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len q) + (len <*r*>) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len q) + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
b19 is ordinal natural finite V38() V45() V46() ext-real set
dom q is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
q /. b19 is Element of the carrier of L
q . b19 is set
p . b19 is set
dom (decomp z) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
p /. b19 is Element of the carrier of L
(decomp z) /. b19 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*p,q*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,p) is Element of the carrier of L
(n,L,(n,L),q) is Element of the carrier of L
(n,L,Pm,p) * (n,L,(n,L),q) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,Pm,p),(n,L,(n,L),q)) is Element of the carrier of L
(n,L,Pm,p) * (0. L) is Element of the carrier of L
the multF of L . ((n,L,Pm,p),(0. L)) is Element of the carrier of L
<*(EmptyBag n),(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
<*<*(EmptyBag n),(EmptyBag n)*>*> is Relation-like NAT -defined (Bags n) * -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of ((Bags n) *) *
((Bags n) *) * is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
0 + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(decomp z) /. b19 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*p,q*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,p) is Element of the carrier of L
(n,L,(n,L),q) is Element of the carrier of L
(n,L,Pm,p) * (n,L,(n,L),q) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,Pm,p),(n,L,(n,L),q)) is Element of the carrier of L
(decomp z) /. 1 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
<*(EmptyBag n),z*> is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(n,L,Pm,(EmptyBag n)) is Element of the carrier of L
(n,L,Pm,(EmptyBag n)) * (0. L) is Element of the carrier of L
the multF of L . ((n,L,Pm,(EmptyBag n)),(0. L)) is Element of the carrier of L
Sum q is Element of the carrier of L
<*> the carrier of L is Relation-like non-empty empty-yielding NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of L *
Sum q is Element of the carrier of L
Sum q is Element of the carrier of L
p . (len p) is set
len q is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len q) + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(q ^ <*r*>) . ((len q) + 1) is set
Sum <*r*> is Element of the carrier of L
(Sum q) + (Sum <*r*>) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((Sum q),(Sum <*r*>)) is Element of the carrier of L
(decomp z) /. (len p) is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p /. (len p) is Element of the carrier of L
b19 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b19,p*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,b19) is Element of the carrier of L
(n,L,(n,L),p) is Element of the carrier of L
(n,L,Pm,b19) * (n,L,(n,L),p) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the multF of L . ((n,L,Pm,b19),(n,L,(n,L),p)) is Element of the carrier of L
<*z,(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(n,L,Pm,z) is Element of the carrier of L
(n,L,Pm,z) * (1. L) is Element of the carrier of L
the multF of L . ((n,L,Pm,z),(1. L)) is Element of the carrier of L
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed doubleLoopStr
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
1. L is V82(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L),Pm) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,(n,L),Pm),z) is Element of the carrier of L
decomp z is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
len (decomp z) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum p is Element of the carrier of L
len p is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom p is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
p . 1 is set
q is Element of the carrier of L
<*q*> is Relation-like NAT -defined the carrier of L -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
r is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
<*q*> ^ r is Relation-like NAT -defined the carrier of L -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum <*q*> is Element of the carrier of L
Sum r is Element of the carrier of L
(Sum <*q*>) + (Sum r) is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . ((Sum <*q*>),(Sum r)) is Element of the carrier of L
<*> the carrier of L is Relation-like non-empty empty-yielding NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of L *
<*> the carrier of L is Relation-like non-empty empty-yielding NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of L *
len r is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
len <*q*> is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len r) + (len <*q*>) is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(len r) + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
b19 is ordinal natural finite V38() V45() V46() ext-real set
dom r is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
r /. b19 is Element of the carrier of L
r . b19 is set
b19 + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
p . (b19 + 1) is set
dom (decomp z) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
p /. (b19 + 1) is Element of the carrier of L
(decomp z) /. (b19 + 1) is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*p,q*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,(n,L),p) is Element of the carrier of L
(n,L,Pm,q) is Element of the carrier of L
(n,L,(n,L),p) * (n,L,Pm,q) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the multF of L . ((n,L,(n,L),p),(n,L,Pm,q)) is Element of the carrier of L
(0. L) * (n,L,Pm,q) is Element of the carrier of L
the multF of L . ((0. L),(n,L,Pm,q)) is Element of the carrier of L
<*(EmptyBag n),(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
<*<*(EmptyBag n),(EmptyBag n)*>*> is Relation-like NAT -defined (Bags n) * -valued Function-like constant non empty trivial Function-yielding V25() finite V40(1) FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of ((Bags n) *) *
((Bags n) *) * is functional non empty FinSequence-membered FinSequenceSet of (Bags n) *
0 + 1 is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
(decomp z) /. (b19 + 1) is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*p,q*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,(n,L),p) is Element of the carrier of L
(n,L,Pm,q) is Element of the carrier of L
(n,L,(n,L),p) * (n,L,Pm,q) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the multF of L . ((n,L,(n,L),p),(n,L,Pm,q)) is Element of the carrier of L
(decomp z) /. (len p) is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
<*z,(EmptyBag n)*> is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(n,L,Pm,(EmptyBag n)) is Element of the carrier of L
(0. L) * (n,L,Pm,(EmptyBag n)) is Element of the carrier of L
the multF of L . ((0. L),(n,L,Pm,(EmptyBag n))) is Element of the carrier of L
<*> the carrier of L is Relation-like non-empty empty-yielding NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of the carrier of L *
(decomp z) /. 1 is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
p /. 1 is Element of the carrier of L
b19 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b19,p*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,(n,L),b19) is Element of the carrier of L
(n,L,Pm,p) is Element of the carrier of L
(n,L,(n,L),b19) * (n,L,Pm,p) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the multF of L . ((n,L,(n,L),b19),(n,L,Pm,p)) is Element of the carrier of L
<*(EmptyBag n),z*> is Relation-like NAT -defined Bags n -valued Function-like non empty Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of (Bags n) *
(n,L,Pm,z) is Element of the carrier of L
(1. L) * (n,L,Pm,z) is Element of the carrier of L
the multF of L . ((1. L),(n,L,Pm,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 ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,y,z) is Element of the carrier of L
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,y,p) is Element of the carrier of L
((Bags n),L,y) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
{} (Bags n) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty proper Function-yielding V25() ordinal natural finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() ext-real V52() V53() V54() V55() V62() V63() V64() V65() V66() V67() V68() FinSequence-yielding finite-support Element of bool (Bags n)
n is 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 right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm + x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
((Bags n),L,Pm) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
((Bags n),L,x) is functional Element of bool (Bags n)
((Bags n),L,Pm) \/ ((Bags n),L,x) is functional Element of bool (Bags n)
((Bags n),L,(n,L,Pm,x)) is functional Element of bool (Bags n)
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
- Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
((Bags n),L,(- Pm)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
((Bags n),L,Pm) is functional Element of bool (Bags n)
y is set
z is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(- Pm),z) is Element of the carrier of L
0. L is V82(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(n,L,Pm,z) is Element of the carrier of L
- (n,L,Pm,z) is Element of the carrier of L
n is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed addLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
- x is Relation-like Bags n -defined Bags n -defined the carrier of L -valued Function-like non empty total total quasi_total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,(- x)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
Pm + (- x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
n is 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 ZeroStr
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
((Bags n),L,(n,L)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
x is set
y is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L),y) is Element of the carrier of L
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive right_unital add-associative right_zeroed doubleLoopStr
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
1. L is V82(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
z is set
y is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
((Bags n),L,y) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
y . z is set
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L),p) is Element of the carrier of L
dom (n,L) is functional non empty Element of bool (Bags n)
{(EmptyBag n)} is functional non empty trivial finite V40(1) set
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,Pm,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
((Bags n),L,Pm) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
((Bags n),L,x) is functional Element of bool (Bags n)
{ H₁(b₁,b₂) where b₁, b₂ is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n : ( b₁ in ((Bags n),L,Pm) & b₂ in ((Bags n),L,x) ) } is set
((Bags n),L,(n,L,Pm,x)) is functional Element of bool (Bags n)
z is set
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,(n,L,Pm,x),p) is Element of the carrier of L
decomp p is Relation-like NAT -defined 2 -tuples_on (Bags n) -valued Function-like one-to-one non empty Function-yielding V25() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags n)
2 -tuples_on (Bags n) is functional non empty FinSequence-membered FinSequenceSet of Bags n
(Bags n) * is functional non empty FinSequence-membered FinSequenceSet of Bags n
{ b₁ where b₁ is Relation-like NAT -defined Bags n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (Bags n) * : len b₁ = 2 } is set
len (decomp p) is non empty ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
q is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum q is Element of the carrier of L
len q is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT
dom q is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
0. L is V82(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
r is ordinal natural finite V38() V45() V46() ext-real set
q /. r is Element of the carrier of L
(decomp p) /. r is Relation-like NAT -defined Bags n -valued Function-like Function-yielding V25() finite V40(2) FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags n)
b19 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
p is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*b19,p*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
(n,L,Pm,b19) is Element of the carrier of L
(n,L,x,p) is Element of the carrier of L
(n,L,Pm,b19) * (n,L,x,p) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((n,L,Pm,b19),(n,L,x,p)) is Element of the carrier of L
dom (decomp p) is non empty finite V62() V63() V64() V65() V66() V67() Element of bool NAT
q is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
a1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
<*q,a1*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like finite-support set
q + a1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support set
n is 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 right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
1. L is V82(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
the Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:] is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
Funcs ((Bags n), the carrier of L) is functional non empty FUNCTION_DOMAIN of Bags n, the carrier of L
bool (Funcs ((Bags n), the carrier of L)) is non empty set
y is functional Element of bool (Funcs ((Bags n), the carrier of L))
z is functional non empty Element of bool (Funcs ((Bags n), the carrier of L))
p is Relation-like Function-like Element of z
q is Relation-like Function-like Element of z
r is Relation-like Bags n -defined the carrier of L -valued Function-like total quasi_total Element of Funcs ((Bags n), the carrier of L)
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
b19 is Relation-like Bags n -defined the carrier of L -valued Function-like total quasi_total Element of Funcs ((Bags n), the carrier of L)
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
a1 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
b1 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,a1,b1) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
a1 + b1 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
O is Relation-like Function-like Element of z
O is Relation-like Function-like Element of z
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
p is Relation-like [:z,z:] -defined z -valued Function-like non empty total quasi_total Function-yielding V25() Element of bool [:[:z,z:],z:]
q is Relation-like Function-like Element of z
r is Relation-like Function-like Element of z
b19 is Relation-like Bags n -defined the carrier of L -valued Function-like total quasi_total Element of Funcs ((Bags n), the carrier of L)
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like Bags n -defined the carrier of L -valued Function-like total quasi_total Element of Funcs ((Bags n), the carrier of L)
a1 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
b1 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
O9 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,b1,O9) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
O is Relation-like Function-like Element of z
R is Relation-like Function-like Element of z
q is Relation-like [:z,z:] -defined z -valued Function-like non empty total quasi_total Function-yielding V25() Element of bool [:[:z,z:],z:]
Pm is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
b19 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
((Bags n),L,p) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
q is set
a1 is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,p,a1) is Element of the carrier of L
r is Relation-like Bags n -defined the carrier of L -valued Function-like total quasi_total Element of Funcs ((Bags n), the carrier of L)
Pm +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
a1 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
b1 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
O is set
O9 is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
((Bags n),L,O9) is functional Element of bool (Bags n)
O9 . O is set
R is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
(n,L,Pm,R) is Element of the carrier of L
dom Pm is functional non empty Element of bool (Bags n)
{(EmptyBag n)} is functional non empty trivial finite V40(1) set
O is Relation-like Bags n -defined the carrier of L -valued Function-like total quasi_total Element of Funcs ((Bags n), the carrier of L)
O is Relation-like Function-like Element of z
q is Relation-like Function-like Element of z
doubleLoopStr(# z,p,q,O,q #) is strict doubleLoopStr
R is non empty strict doubleLoopStr
the carrier of R is non empty set
0. R is V82(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
1. R is Element of the carrier of R
the OneF of R is Element of the carrier of R
x is set
y is Relation-like Bags n -defined the carrier of L -valued Function-like total quasi_total Element of Funcs ((Bags n), the carrier of L)
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Element of the carrier of R
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
y is Element of the carrier of R
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
p . (x,y) is set
x + y is Element of the carrier of R
the addF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is Relation-like non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . (x,y) is Element of the carrier of R
(n,L,p,q) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
p + q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
vdbl is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
vdbr is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
rs is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,vdbl,vdbr) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
vdbl + vdbr is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x is Element of the carrier of R
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
y is Element of the carrier of R
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
q . (x,y) is set
x * y is Element of the carrier of R
the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . (x,y) is Element of the carrier of R
(n,L,p,q) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
vdbl is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
vdbr is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
rs is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,vdbl,vdbr) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
Pm is non empty strict doubleLoopStr
the carrier of Pm is non empty set
0. Pm is V82(Pm) Element of the carrier of Pm
the ZeroF of Pm is Element of the carrier of Pm
1. Pm is Element of the carrier of Pm
the OneF of Pm is Element of the carrier of Pm
x is non empty strict doubleLoopStr
the carrier of x is non empty set
0. x is V82(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
1. x is Element of the carrier of x
the OneF of x is Element of the carrier of x
y is set
y is Element of the carrier of Pm
z is Element of the carrier of Pm
p is Element of the carrier of x
q is Element of the carrier of x
the multF of Pm is Relation-like [: the carrier of Pm, the carrier of Pm:] -defined the carrier of Pm -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of Pm, the carrier of Pm:], the carrier of Pm:]
[: the carrier of Pm, the carrier of Pm:] is Relation-like non empty set
[:[: the carrier of Pm, the carrier of Pm:], the carrier of Pm:] is Relation-like non empty set
bool [:[: the carrier of Pm, the carrier of Pm:], the carrier of Pm:] is non empty set
the multF of Pm . (y,z) is Element of the carrier of Pm
a1 is Element of the carrier of Pm
b1 is Element of the carrier of Pm
a1 * b1 is Element of the carrier of Pm
the multF of Pm . (a1,b1) is Element of the carrier of Pm
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,q) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
r is Element of the carrier of x
b19 is Element of the carrier of x
r * b19 is Element of the carrier of x
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the multF of x . (r,b19) is Element of the carrier of x
the multF of x . (y,z) is set
y is Element of the carrier of Pm
z is Element of the carrier of Pm
p is Element of the carrier of x
q is Element of the carrier of x
the addF of Pm is Relation-like [: the carrier of Pm, the carrier of Pm:] -defined the carrier of Pm -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of Pm, the carrier of Pm:], the carrier of Pm:]
the addF of Pm . (y,z) is Element of the carrier of Pm
a1 is Element of the carrier of Pm
b1 is Element of the carrier of Pm
a1 + b1 is Element of the carrier of Pm
the addF of Pm . (a1,b1) is Element of the carrier of Pm
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,q) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
p + q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
r is Element of the carrier of x
b19 is Element of the carrier of x
r + b19 is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the addF of x . (r,b19) is Element of the carrier of x
the addF of x . (y,z) is set
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
(n,L) is non empty strict doubleLoopStr
the carrier of (n,L) is non empty set
x is Element of the carrier of (n,L)
y is Element of the carrier of (n,L)
x + y is Element of the carrier of (n,L)
the addF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the addF of (n,L) . (x,y) is Element of the carrier of (n,L)
y + x is Element of the carrier of (n,L)
the addF of (n,L) . (y,x) is Element of the carrier of (n,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 non trivial set
[:(Bags n), the carrier of L:] is Relation-like 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 non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,z) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
p + z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
(n,L) is non empty strict doubleLoopStr
the carrier of (n,L) is non empty set
x is Element of the carrier of (n,L)
y is Element of the carrier of (n,L)
x + y is Element of the carrier of (n,L)
the addF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the addF of (n,L) . (x,y) is Element of the carrier of (n,L)
z is Element of the carrier of (n,L)
(x + y) + z is Element of the carrier of (n,L)
the addF of (n,L) . ((x + y),z) is Element of the carrier of (n,L)
y + z is Element of the carrier of (n,L)
the addF of (n,L) . (y,z) is Element of the carrier of (n,L)
x + (y + z) is Element of the carrier of (n,L)
the addF of (n,L) . (x,(y + z)) is Element of the carrier of (n,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 non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
r is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,q,r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
q + r is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,q) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
p + q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,p,q),r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,q) + r is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,p,(n,L,q,r)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
p + (n,L,q,r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
(n,L) is non empty strict add-associative doubleLoopStr
the carrier of (n,L) is non empty set
Pm is Element of the carrier of (n,L)
0. (n,L) is V82((n,L)) Element of the carrier of (n,L)
the ZeroF of (n,L) is Element of the carrier of (n,L)
Pm + (0. (n,L)) is Element of the carrier of (n,L)
the addF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the addF of (n,L) . (Pm,(0. (n,L))) is Element of the carrier of (n,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 non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,x,(n,L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
x + (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like right-distributive left-distributive right_unital distributive add-associative right_zeroed doubleLoopStr
(n,L) is non empty strict add-associative right_zeroed doubleLoopStr
the carrier of (n,L) is non empty set
Pm is Element of the carrier of (n,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 non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
x is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
- x is Relation-like Bags n -defined Bags n -defined the carrier of L -valued Function-like non empty total total quasi_total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
y is Element of the carrier of (n,L)
Pm + y is Element of the carrier of (n,L)
the addF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the addF of (n,L) . (Pm,y) is Element of the carrier of (n,L)
0. (n,L) is V82((n,L)) Element of the carrier of (n,L)
the ZeroF of (n,L) is Element of the carrier of (n,L)
(n,L,x,x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L,x,(- x)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
x + (- x) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like commutative right-distributive left-distributive right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
(n,L) is non empty left_add-cancelable right_add-cancelable right_complementable strict left_zeroed add-left-invertible add-right-invertible Loop-like Abelian add-associative right_zeroed doubleLoopStr
the carrier of (n,L) is non empty set
x is Element of the carrier of (n,L)
y is Element of the carrier of (n,L)
x * y is Element of the carrier of (n,L)
the multF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the multF of (n,L) . (x,y) is Element of the carrier of (n,L)
y * x is Element of the carrier of (n,L)
the multF of (n,L) . (y,x) is Element of the carrier of (n,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 non trivial set
[:(Bags n), the carrier of L:] is Relation-like 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 non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,z) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like associative right-distributive left-distributive right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
(n,L) is non empty left_add-cancelable right_add-cancelable right_complementable strict left_zeroed add-left-invertible add-right-invertible Loop-like Abelian add-associative right_zeroed doubleLoopStr
the carrier of (n,L) is non empty set
x is Element of the carrier of (n,L)
y is Element of the carrier of (n,L)
x * y is Element of the carrier of (n,L)
the multF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the multF of (n,L) . (x,y) is Element of the carrier of (n,L)
z is Element of the carrier of (n,L)
(x * y) * z is Element of the carrier of (n,L)
the multF of (n,L) . ((x * y),z) is Element of the carrier of (n,L)
y * z is Element of the carrier of (n,L)
the multF of (n,L) . (y,z) is Element of the carrier of (n,L)
x * (y * z) is Element of the carrier of (n,L)
the multF of (n,L) . (x,(y * z)) is Element of the carrier of (n,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 non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
r is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,q,r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
p is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,q) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,p,q),r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,(n,L,q,r)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(n,L) is non empty left_add-cancelable right_add-cancelable right_complementable strict left_zeroed add-left-invertible add-right-invertible Loop-like associative Abelian add-associative right_zeroed doubleLoopStr
the carrier of (n,L) is non empty 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
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
x is Element of the carrier of (n,L)
y is Element of the carrier of (n,L)
1. (n,L) is Element of the carrier of (n,L)
the OneF of (n,L) is Element of the carrier of (n,L)
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
1. L is V82(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x * y is Element of the carrier of (n,L)
the multF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the multF of (n,L) . (x,y) is Element of the carrier of (n,L)
z is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,z,(n,L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
y * x is Element of the carrier of (n,L)
the multF of (n,L) . (y,x) is Element of the carrier of (n,L)
(n,L,(n,L),z) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
(n,L) is non empty left_add-cancelable right_add-cancelable right_complementable strict left_zeroed add-left-invertible add-right-invertible Loop-like associative Abelian add-associative right_zeroed doubleLoopStr
the carrier of (n,L) is non empty set
x is Element of the carrier of (n,L)
1. (n,L) is Element of the carrier of (n,L)
the OneF of (n,L) is Element of the carrier of (n,L)
x * (1. (n,L)) is Element of the carrier of (n,L)
the multF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the multF of (n,L) . (x,(1. (n,L))) is Element of the carrier of (n,L)
(1. (n,L)) * x is Element of the carrier of (n,L)
the multF of (n,L) . ((1. (n,L)),x) is Element of the carrier of (n,L)
the carrier of (n,L) is non empty set
x is Element of the carrier of (n,L)
y is Element of the carrier of (n,L)
z is Element of the carrier of (n,L)
y + z is Element of the carrier of (n,L)
the addF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
[: the carrier of (n,L), the carrier of (n,L):] is Relation-like non empty set
[:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is Relation-like non empty set
bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):] is non empty set
the addF of (n,L) . (y,z) is Element of the carrier of (n,L)
x * (y + z) is Element of the carrier of (n,L)
the multF of (n,L) is Relation-like [: the carrier of (n,L), the carrier of (n,L):] -defined the carrier of (n,L) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (n,L), the carrier of (n,L):], the carrier of (n,L):]
the multF of (n,L) . (x,(y + z)) is Element of the carrier of (n,L)
x * y is Element of the carrier of (n,L)
the multF of (n,L) . (x,y) is Element of the carrier of (n,L)
x * z is Element of the carrier of (n,L)
the multF of (n,L) . (x,z) is Element of the carrier of (n,L)
(x * y) + (x * z) is Element of the carrier of (n,L)
the addF of (n,L) . ((x * y),(x * z)) is Element of the carrier of (n,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 non trivial set
[:(Bags n), the carrier of L:] is Relation-like 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 non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
q is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,q) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
r is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
y + z is Element of the carrier of (n,L)
(n,L,q,r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
q + r is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
x * (y + z) is Element of the carrier of (n,L)
the multF of (n,L) . (x,(y + z)) is Element of the carrier of (n,L)
(n,L,p,(n,L,q,r)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,p,q),(n,L,p,r)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
(n,L,p,q) + (n,L,p,r) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]
(x * y) + (x * z) is Element of the carrier of (n,L)
n is ordinal set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like associative right-distributive left-distributive right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
(n,L) is non empty left_add-cancelable right_add-cancelable right_complementable strict left_zeroed add-left-invertible add-right-invertible Loop-like associative Abelian add-associative right_zeroed doubleLoopStr
1. (n,L) is Element of the carrier of (n,L)
the carrier of (n,L) is non empty set
the OneF of (n,L) is Element of the carrier of (n,L)
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags 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
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is Relation-like non empty set
bool [:(Bags n), the carrier of L:] is non empty set
(n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total ( Bags n,L) Element of bool [:(Bags n), the carrier of L:]
0. L is V82(L) 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 quasi_total Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V40(1) set
[:(Bags n),{(0. L)}:] is Relation-like non empty set
EmptyBag n is Relation-like n -defined RAT -valued Function-like total V52() V53() V54() V55() finite-support Element of Bags n
1. L is V82(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
(n,L) +* ((EmptyBag n),(1. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like non empty total quasi_total Element of bool [:(Bags n), the carrier of L:]