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

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
is Relation-like V52() V53() V54() set
bool 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

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

the carrier of n is non empty set

dom 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

dom (L + Pm) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT

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
the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet 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
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 functional non empty FinSequence-membered FinSequenceSet of the carrier of n *

dom (Sum (<*> ( the carrier of n *))) is finite V62() V63() V64() V65() V66() V67() Element of bool NAT

the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

Sum L is Element of the carrier of n

( the carrier of n *) * is functional non empty FinSequence-membered FinSequenceSet 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

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
the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet 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

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

Sum (L /. x) is Element of the carrier of n

Sum ((L ^ Pm) /. x) is Element of the carrier of n

(len L) + y is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT

(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

Sum (Pm /. y) is 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

Pm is Element 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
() * 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

dom y is finite V62() V63() V64() V65() V66() V67() Element of bool NAT
z is set
y . z is set
(() * 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
() . (L /. z) is Element of the carrier of n
L . z is set
() . (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 () is non empty Element of bool the carrier of n
dom (() * 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
(() * L) . y is set
L . y is set
() . (L . y) is set
() . (L /. y) is Element 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

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

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

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

dom x is finite V62() V63() V64() V65() V66() V67() Element of bool NAT

dom y is finite V62() V63() V64() V65() V66() V67() Element of bool NAT

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 functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Element of the carrier of n

dom (L * (<*> the carrier of n)) 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

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

n is non empty multMagma
the carrier of n is non empty set
Pm is 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 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

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

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
L is Element 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

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

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

(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

(len Pm) + z is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT

(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

(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) ^ (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

(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

(len Pm) + z is ordinal natural finite V38() V45() V46() ext-real V50() V51() V62() V63() V64() V65() V66() V67() Element of NAT

(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

the carrier of n is non empty set
L is Element of the carrier of n

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet 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

Sum (L * (x ^ <*y*>)) is Element 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

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 * () is Element of the carrier of n
the multF of n . (L,()) is Element of the carrier of n
(L * (Sum x)) + (L * ()) is Element of the carrier of n
the addF of n . ((L * (Sum x)),(L * ())) is Element of the carrier of n
(Sum x) + () is Element of the carrier of n
the addF 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 . (L,((Sum x) + ())) 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

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

the carrier of n is non empty set
L is Element of the carrier of n

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet 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

Sum (n,(x ^ <*y*>),L) is Element 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

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
() * L is Element of the carrier of n
the multF of n . ((),L) is Element of the carrier of n
((Sum x) * L) + (() * L) is Element of the carrier of n
the addF of n . (((Sum x) * L),(() * L)) is Element of the carrier of n
(Sum x) + () is Element of the carrier of n
the addF 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 . (((Sum x) + ()),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

the carrier of n is non empty set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

Sum () is Element of the carrier of n

Sum (Sum L) is Element of the carrier of n

( the carrier of n *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n *

Sum (FlattenSeq (L ^ <*Pm*>)) is Element of the carrier of n

Sum (Sum (L ^ <*Pm*>)) is Element of the carrier of n

Sum (() ^ ()) is Element of the carrier of n

Sum (() ^ 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 <*(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 ((Sum L) ^ <*(Sum Pm)*>) is Element of the carrier of n

Sum ((Sum L) ^ (Sum <*Pm*>)) is Element of the carrier of n

( the carrier of n *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n *

Sum (FlattenSeq (<*> ( the carrier of n *))) is Element of the carrier of n

Sum (<*> the carrier of n) is Element 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:]

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

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

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

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

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

(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

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

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

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)

(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

(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