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