:: POLYNOM7 semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

[:2,2:] is non empty finite set
[:[:2,2:],2:] is non empty finite set
bool [:[:2,2:],2:] is non empty finite V33() set

{{},1} is non empty finite V33() set

RAT is set
INT is set
is non empty non trivial non finite set
bool is non empty non trivial non finite set

Seg 1 is Element of bool NAT
{1} is non empty trivial finite V33() V36(1) set
Seg 2 is Element of bool NAT
{1,2} is non empty finite V33() set

Bags {} is functional non empty Element of bool ()
Bags {} is non empty set
bool () is non empty set
is non empty trivial finite V33() V36(1) set

n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty non trivial ZeroStr
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
{(0. L)} is non empty trivial finite V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
the Element of NonZero L is Element of NonZero L
{(0. L)} is non empty trivial finite V36(1) Element of bool the carrier of L
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

a is Element of the carrier of L
(0_ (n,L)) +* ((),a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
[:(Bags n),{(0. L)}:] is non empty set
dom (0_ (n,L)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
r . () is Element of the carrier of L

Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty non trivial ZeroStr
the carrier of L is non empty non trivial set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
{(0. L)} is non empty trivial finite V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
the Element of NonZero L is Element of NonZero L
{(0. L)} is non empty trivial finite V36(1) Element of bool the carrier of L
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support Element of bool [:(Bags n), the carrier of L:]

a is Element of the carrier of L
(0_ (n,L)) +* ((),a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
q is set
r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
Support r is functional Element of bool (Bags n)
bool (Bags n) is non empty set
r . q is set
(0_ (n,L)) . q is set
{()} is functional non empty trivial finite V36(1) Element of bool (Bags n)
(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
[:(Bags n),{(0. L)}:] is non empty set
dom (0_ (n,L)) is functional Element of bool (Bags n)
r . () is Element of the carrier of L
q is set
q is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support Element of bool [:(Bags n), the carrier of L:]
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
Support p is functional Element of bool (Bags n)
bool (Bags n) is non empty set
a is set

p . x is Element of the carrier of L
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
p . a is set
(0_ (n,L)) . a is set
dom p is functional Element of bool (Bags n)
dom (0_ (n,L)) is functional Element of bool (Bags n)

p . x is Element of the carrier of L
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set

0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
{(0. L)} is non empty trivial finite V36(1) set
a is set
{(0. L)} is non empty trivial finite V36(1) Element of bool the carrier of L
bool the carrier of L is non empty set
a is set
a is set
{a} is non empty trivial finite V36(1) set
a is Element of the carrier of L
a is Element of the carrier of L
(Bags n) --> a is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{a} is non empty trivial finite V36(1) set
[:(Bags n),{a}:] is non empty set
y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
q is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
q . () is Element of the carrier of L
Support q is functional Element of bool (Bags n)
bool (Bags n) is non empty set
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
Support p is functional Element of bool (Bags n)
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
Support p is functional Element of bool (Bags n)

y is set
{y} is non empty trivial finite V36(1) set
y is set
{y} is non empty trivial finite V36(1) set

p . x is Element of the carrier of L
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
Support p is functional Element of bool (Bags n)
x is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
Support x is functional Element of bool (Bags n)
n is set
n is non empty set
the Element of n is Element of n

Bags n is non empty set
Bags n is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
() +* ( the Element of n,1) is Relation-like n -defined Function-like total V208() finite-support set
dom () is Element of bool n
bool n is non empty set
(() +* ( the Element of n,1)) . the Element of n is set

{ the Element of n} is non empty trivial finite V36(1) set
{ the Element of n} --> 1 is Relation-like non-empty { the Element of n} -defined NAT -valued {1} -valued Function-like constant non empty total V18({ the Element of n},{1}) finite finite-support Element of bool [:{ the Element of n},{1}:]
[:{ the Element of n},{1}:] is non empty finite set
bool [:{ the Element of n},{1}:] is non empty finite V33() set
() +* ( the Element of n .--> 1) is Relation-like Function-like set
(() +* ( the Element of n .--> 1)) . the Element of n is set
dom ( the Element of n .--> 1) is finite Element of bool n
{ the Element of n} is non empty trivial finite V36(1) Element of bool n
support (() +* ( the Element of n,1)) is finite set
a is set
(() +* ( the Element of n,1)) . a is set
(() +* ( the Element of n .--> 1)) . a is set
() . a is set
( the Element of n .--> 1) . the Element of n is set
a is set
n is non empty set

p is Element of n
{p} is non empty trivial finite V36(1) Element of bool n
bool n is non empty set
L . p is set

Bags n is non empty set
Bags n is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
() . p is set

{()} is functional non empty trivial finite V36(1) Element of bool ()
bool () is non empty set
L is non empty doubleLoopStr
the carrier of L is non empty set
[:(), the carrier of L:] is non empty set
bool [:(), the carrier of L:] is non empty set
p is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]

[:, the carrier of L:] is non empty set
bool [:, the carrier of L:] is non empty set
a is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]
x is Relation-like -defined the carrier of L -valued Function-like V18(, the carrier of L) finite finite-support Element of bool [:, the carrier of L:]
x /. {} is Element of the carrier of L

bool is non empty finite V33() set
{(x /. {})} is non empty trivial finite V36(1) Element of bool the carrier of L
bool the carrier of L is non empty set
[:{()},{(x /. {})}:] is non empty finite set
z is set
r is set
q is set
[r,q] is set

x . {} is set
{()} --> (x /. {}) is Relation-like {()} -defined the carrier of L -valued Function-like constant non empty total V18({()}, the carrier of L) finite finite-support Element of bool [:{()}, the carrier of L:]
[:{()}, the carrier of L:] is non empty set
bool [:{()}, the carrier of L:] is non empty set
{(x /. {})} is non empty trivial finite V36(1) set
[:{()},{(x /. {})}:] is non empty finite set
z is set
r is set
q is set
[r,q] is set
x . {} is set

the carrier of L is non empty non trivial set
[:(), the carrier of L:] is non empty set
bool [:(), the carrier of L:] is non empty set
[:{}, the carrier of L:] is set
bool [:{}, the carrier of L:] is non empty set
p is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]

{()} --> x is Relation-like {()} -defined the carrier of L -valued Function-like constant non empty total V18({()}, the carrier of L) finite finite-support Element of bool [:{()}, the carrier of L:]
[:{()}, the carrier of L:] is non empty set
bool [:{()}, the carrier of L:] is non empty set
{x} is non empty trivial finite V36(1) set
[:{()},{x}:] is non empty finite set
dom p is functional Element of bool ()

[:(),():] is non empty set
bool [:(),():] is non empty set

p * (SgmX ((),())) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
[:NAT, the carrier of L:] is non empty non trivial non finite set
bool [:NAT, the carrier of L:] is non empty non trivial non finite set

K468( the carrier of L) is M35( the carrier of L)

[:(),():] is non empty set
bool [:(),():] is non empty set

r is set

r is set
rng (SgmX ((),y)) is set
dom (SgmX ((),y)) is Element of bool NAT
(SgmX ((),y)) . 1 is Relation-like Function-like set
p * (SgmX ((),y)) is Relation-like NAT -defined the carrier of L -valued Function-like Element of bool [:NAT, the carrier of L:]
[:NAT, the carrier of L:] is non empty non trivial non finite set
bool [:NAT, the carrier of L:] is non empty non trivial non finite set
dom (p * (SgmX ((),y))) is Element of bool NAT
(p * (SgmX ((),y))) /. 1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
(p * (SgmX ((),y))) . 1 is set
p . ((SgmX ((),y)) . 1) is set
{1} is non empty trivial finite V33() V36(1) Element of bool NAT
r is set

(SgmX ((),y)) . q is Relation-like Function-like set

Seg r is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V28() finite V34() ext-real V174() Element of NAT : ( 1 <= b1 & b1 <= r ) } is set

r is set

dom r is Element of bool NAT
Seg (len r) is Element of bool NAT
r . 1 is set

eval ((((SgmX ((),y)) /. 1) @),a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
((p * (SgmX ((),y))) /. 1) * (eval ((((SgmX ((),y)) /. 1) @),a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

((p * (SgmX ((),y))) /. 1) * (eval ((),a)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

((p * (SgmX ((),y))) /. 1) * (1. L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*x*> is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like M36( the carrier of L,K468( the carrier of L))
K468( the carrier of L) is M35( the carrier of L)

the carrier of L is non empty non trivial set
[:(), the carrier of L:] is non empty set
bool [:(), the carrier of L:] is non empty set
0_ ({},L) is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
dom (0_ ({},L)) is functional Element of bool ()

{()} --> (1_ L) is Relation-like {()} -defined the carrier of L -valued {(1_ L)} -valued Function-like constant non empty total V18({()},{(1_ L)}) finite finite-support Element of bool [:{()},{(1_ L)}:]
{(1_ L)} is non empty trivial finite V36(1) set
[:{()},{(1_ L)}:] is non empty finite set
bool [:{()},{(1_ L)}:] is non empty finite V33() set
dom (() .--> (1_ L)) is functional trivial finite Element of bool {()}
bool {()} is non empty finite V33() set

the carrier of (Polynom-Ring ({},L)) is non empty set

y is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
y . {} is set
dom y is functional Element of bool ()
rng y is set
[: the carrier of (Polynom-Ring ({},L)), the carrier of L:] is non empty set
bool [: the carrier of (Polynom-Ring ({},L)), the carrier of L:] is non empty set
x is Relation-like the carrier of (Polynom-Ring ({},L)) -defined the carrier of L -valued Function-like V18( the carrier of (Polynom-Ring ({},L)), the carrier of L) Element of bool [: the carrier of (Polynom-Ring ({},L)), the carrier of L:]
dom x is Element of bool the carrier of (Polynom-Ring ({},L))
bool the carrier of (Polynom-Ring ({},L)) is non empty set

the OneF of (Polynom-Ring ({},L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring ({},L))
y is Relation-like the carrier of (Polynom-Ring ({},L)) -defined the carrier of L -valued Function-like V18( the carrier of (Polynom-Ring ({},L)), the carrier of L) Element of bool [: the carrier of (Polynom-Ring ({},L)), the carrier of L:]

z is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
z . {} is set
1_ ({},L) is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
(0_ ({},L)) +* ((),(1_ L)) is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]

(y . r) * (y . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
r . {} is set
q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
q . {} is set
r *' q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
(r *' q) . {} is set

(r . a) * (q . a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

K469(2,()) is M35( Bags {})
[:NAT,():] is non empty non trivial non finite set
bool [:NAT,():] is non empty non trivial non finite set

K468(()) is M35( Bags {})

K468(()) is M35( bool [:NAT,():])

dom k is Element of bool NAT

<*c,c*> is set

(r . c) * (q . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
k . 1 is set
(r . a) * (q . c) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
<*((r . a) * (q . a))*> is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like M36( the carrier of L,K468( the carrier of L))
K468( the carrier of L) is M35( the carrier of L)
i is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
i . {} is set

(y . r) + (y . q) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
r is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
r . {} is set
q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
q . {} is set

{()} --> i is Relation-like {()} -defined the carrier of L -valued Function-like constant non empty total V18({()}, the carrier of L) finite finite-support Element of bool [:{()}, the carrier of L:]
[:{()}, the carrier of L:] is non empty set
bool [:{()}, the carrier of L:] is non empty set
{i} is non empty trivial finite V36(1) set
[:{()},{i}:] is non empty finite set

{()} --> k is Relation-like {()} -defined the carrier of L -valued Function-like constant non empty total V18({()}, the carrier of L) finite finite-support Element of bool [:{()}, the carrier of L:]
{k} is non empty trivial finite V36(1) set
[:{()},{k}:] is non empty finite set
r + q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
(r + q) . {} is set

(r . a) + (q . a) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
c . {} is set

(0_ ({},L)) +* (() .--> (1_ L)) is Relation-like Function-like set
((0_ ({},L)) +* (() .--> (1_ L))) . () is set
(() .--> (1_ L)) . () is set
rng y is set
r is set

{q} is non empty trivial finite V36(1) set
[:{()},{q}:] is non empty finite set
bool [:{()},{q}:] is non empty finite V33() set

dom q is set
rng q is set
{q} is non empty trivial finite V36(1) Element of bool the carrier of L
bool the carrier of L is non empty set
i is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]
k is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]

c is set

c is set

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) Element of bool [:(), the carrier of L:]

c is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]

q is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
q . {} is set

r is set
dom y is Element of bool the carrier of (Polynom-Ring ({},L))
r is set
q is set
y . r is set
y . q is set

i is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
i . {} is set

k is Relation-like Bags {} -defined the carrier of L -valued Function-like V18( Bags {}, the carrier of L) finite-Support Element of bool [:(), the carrier of L:]
k . {} is set

{()} --> c is Relation-like {()} -defined the carrier of L -valued Function-like constant non empty total V18({()}, the carrier of L) finite finite-support Element of bool [:{()}, the carrier of L:]
[:{()}, the carrier of L:] is non empty set
bool [:{()}, the carrier of L:] is non empty set
{c} is non empty trivial finite V36(1) set
[:{()},{c}:] is non empty finite set

{()} --> c is Relation-like {()} -defined the carrier of L -valued Function-like constant non empty total V18({()}, the carrier of L) finite finite-support Element of bool [:{()}, the carrier of L:]
{c} is non empty trivial finite V36(1) set
[:{()},{c}:] is non empty finite set
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L

(0_ (n,L)) . a is Element of the carrier of L
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L

p . a is Element of the carrier of L
Support p is functional Element of bool (Bags n)
bool (Bags n) is non empty set
x is functional non empty Element of bool (Bags n)

p . the Relation-like n -defined Function-like total V208() finite-support Element of x is Element of the carrier of L
p . a is Element of the carrier of L
x is set
Support p is functional Element of bool (Bags n)
bool (Bags n) is non empty set

p . y is Element of the carrier of L
{a} is functional non empty trivial finite V36(1) set
x is set

p . a is Element of the carrier of L
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
Support p is functional Element of bool (Bags n)
bool (Bags n) is non empty set

{a} is functional non empty trivial finite V36(1) set

{a} is functional non empty trivial finite V36(1) set
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L

p . x is Element of the carrier of L

p . a is Element of the carrier of L
{a} is functional non empty trivial finite V36(1) set
x is set

p . y is Element of the carrier of L
x is set
p . x is set

p . a is Element of the carrier of L
x is functional non empty Element of bool (Bags n)

p . the Relation-like n -defined Function-like total V208() finite-support Element of x is Element of the carrier of L
p . a is Element of the carrier of L
p . a is Element of the carrier of L

{x} is functional non empty trivial finite V36(1) set

p . x is Element of the carrier of L

{a} is functional non empty trivial finite V36(1) set

{x} is functional non empty trivial finite V36(1) set
L is non empty ZeroStr
the carrier of L is non empty set
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set

p is Element of the carrier of L
(0_ (n,L)) +* (a,p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{a} is functional non empty trivial finite V36(1) set

{p} is non empty trivial finite V36(1) set
[:{a},{p}:] is non empty finite set
bool [:{a},{p}:] is non empty finite V33() set
dom (a .--> p) is functional trivial finite Element of bool {a}
bool {a} is non empty finite V33() set
y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
dom (0_ (n,L)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V36(1) set
[:(Bags n),{(0. L)}:] is non empty set
dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)
r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* (a .--> p) is Relation-like Function-like set
r . a is Element of the carrier of L
((0_ (n,L)) +* (a .--> p)) . a is set
(a .--> p) . a is set
Support r is functional Element of bool (Bags n)
q is set

r . r is Element of the carrier of L
(0_ (n,L)) . r is Element of the carrier of L
q is set
Support r is functional Element of bool (Bags n)
q is functional non empty Element of bool (Bags n)

r . the Relation-like n -defined Function-like total V208() finite-support Element of q is Element of the carrier of L

r . q is Element of the carrier of L
(0_ (n,L)) . q is Element of the carrier of L
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
Support p is functional Element of bool (Bags n)
bool (Bags n) is non empty set

p . a is Element of the carrier of L
p . a is Element of the carrier of L
x is functional non empty Element of bool (Bags n)

p . the Relation-like n -defined Function-like total V208() finite-support Element of x is Element of the carrier of L
p . a is Element of the carrier of L
p . a is Element of the carrier of L

p . x is Element of the carrier of L

p . z is Element of the carrier of L

p . a is Element of the carrier of L

p . x is Element of the carrier of L

n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]

p . (n,L,p) is Element of the carrier of L
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]
Support p is functional Element of bool (Bags n)
bool (Bags n) is non empty set

{(n,L,p)} is functional non empty trivial finite V36(1) set
p . (n,L,p) is Element of the carrier of L
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L

{a} is functional non empty trivial finite V36(1) set
n is set

Bags n is non empty set
Bags n is functional non empty Element of bool (Bags n)
bool (Bags n) is non empty set
L is non empty ZeroStr
0. L is zero Element of the carrier of L
the carrier of L is non empty set
the ZeroF of L is Element of the carrier of L

(n,L,(0. L),p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* (p,(0. L)) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,(0. L),p)) is Element of the carrier of L
(n,L,(n,L,(0. L),p)) is Relation-like n -defined Function-like total V208() finite-support set
(n,L,(0. L),p) . (n,L,(n,L,(0. L),p)) is Element of the carrier of L
x is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
dom (0_ (n,L)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V36(1) set
[:(Bags n),{(0. L)}:] is non empty set
dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)
z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]

{p} is functional non empty trivial finite V36(1) set
{p} --> (0. L) is Relation-like {p} -defined the carrier of L -valued {(0. L)} -valued Function-like constant non empty total V18({p},{(0. L)}) finite finite-support Element of bool [:{p},{(0. L)}:]
[:{p},{(0. L)}:] is non empty finite set
bool [:{p},{(0. L)}:] is non empty finite V33() set
(0_ (n,L)) +* (p .--> (0. L)) is Relation-like Function-like set
dom (p .--> (0. L)) is functional trivial finite Element of bool {p}
bool {p} is non empty finite V33() set
z . p is Element of the carrier of L
((0_ (n,L)) +* (p .--> (0. L))) . p is set
(p .--> (0. L)) . p is set

z . r is Element of the carrier of L

z . r is Element of the carrier of L
(0_ (n,L)) . r is Element of the carrier of L

z . r is Element of the carrier of L

z . r is Element of the carrier of L
n is set
L is non empty ZeroStr
the carrier of L is non empty set
p is Element of the carrier of L

(n,L,p,a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* (a,p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,p,a)) is Element of the carrier of L
(n,L,(n,L,p,a)) is Relation-like n -defined Function-like total V208() finite-support set
(n,L,p,a) . (n,L,(n,L,p,a)) is Element of the carrier of L
y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{a} is functional non empty trivial finite V36(1) set

{p} is non empty trivial finite V36(1) set
[:{a},{p}:] is non empty finite set
bool [:{a},{p}:] is non empty finite V33() set
dom (a .--> p) is functional trivial finite Element of bool {a}
bool {a} is non empty finite V33() set
dom (0_ (n,L)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V36(1) set
[:(Bags n),{(0. L)}:] is non empty set
dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)
r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
r . a is Element of the carrier of L
(0_ (n,L)) +* (a .--> p) is Relation-like Function-like set
((0_ (n,L)) +* (a .--> p)) . a is set
(a .--> p) . a is set
n is set
L is non empty non trivial ZeroStr
the carrier of L is non empty non trivial set
p is non zero Element of the carrier of L

(n,L,p,a) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(Bags n), the carrier of L:]
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
0_ (n,L) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(0_ (n,L)) +* (a,p) is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
(n,L,(n,L,p,a)) is Relation-like n -defined Function-like total V208() finite-support set
y is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
z is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{a} is functional non empty trivial finite V36(1) set

{p} is non empty trivial finite V36(1) set
[:{a},{p}:] is non empty finite set
bool [:{a},{p}:] is non empty finite V33() set
dom (a .--> p) is functional trivial finite Element of bool {a}
bool {a} is non empty finite V33() set
dom (0_ (n,L)) is functional Element of bool (Bags n)
bool (Bags n) is non empty set
0. L is zero Element of the carrier of L
the ZeroF of L is Element of the carrier of L
(Bags n) --> (0. L) is Relation-like Bags n -defined the carrier of L -valued Function-like constant non empty total V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
{(0. L)} is non empty trivial finite V36(1) set
[:(Bags n),{(0. L)}:] is non empty set
dom ((Bags n) --> (0. L)) is functional Element of bool (Bags n)
r is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) Element of bool [:(Bags n), the carrier of L:]
r . a is Element of the carrier of L
(0_ (n,L)) +* (a .--> p) is Relation-like Function-like set
((0_ (n,L)) +* (a .--> p)) . a is set
(a .--> p) . a is set
n is set
Bags n is functional non empty Element of bool (Bags n)
Bags n is non empty set
bool (Bags n) is non empty set
L is non empty ZeroStr
the carrier of L is non empty set
[:(Bags n), the carrier of L:] is non empty set
bool [:(Bags n), the carrier of L:] is non empty set
p is Relation-like Bags n -defined the carrier of L -valued Function-like V18( Bags n, the carrier of L) finite-Support (n,L) Element of bool [:(