:: 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