:: POLYNOM2 semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K124(NAT) is V33() set

RAT is set
INT is set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is non empty non trivial Relation-like non finite set
is non empty non trivial Relation-like non finite set
bool is non empty non trivial non finite set
K266() is set

{{},1} is non empty finite V38() set
K624() is non empty strict multMagma
the carrier of K624() is non empty set
K629() is non empty strict unital Group-like associative commutative V243() V244() V245() V246() V247() V248() multMagma
K630() is non empty strict associative commutative V246() V247() V248() M37(K629())
K631() is non empty strict unital associative commutative V246() V247() V248() V249() M40(K629(),K630())

K634() is non empty strict unital associative commutative V249() M37(K633())

bool is non empty set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial finite V38() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{1,2} is non empty finite V38() set

Bags {} is non empty functional Element of bool ()
Bags {} is non empty set
bool () is non empty set
is non empty trivial functional finite V38() 1 -element set
n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set
L is Element of bool n

field x is set
f is set
p is set
[f,p] is set
[p,f] is set
f is set
p is set
q is set
[f,p] is set
[p,q] is set
[f,q] is set
f is set
[f,f] is set
n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set
L is Element of bool n

f is set
p is set
[f,p] is set
[p,f] is set
n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set
L is Element of bool n

field x is set
f is set
p is set
q is set
[f,p] is set
[p,q] is set
[f,q] is set
f is set
p is set
[f,p] is set
[p,f] is set
f is set
p is set
[f,p] is set
[p,f] is set
dom x is Element of bool n
rng x is Element of bool n
(dom x) \/ (rng x) is Element of bool n
[p,p] is set
[f,f] is set
f is set
[f,f] is set
n is non empty unital associative multMagma
the carrier of n is non empty set
power n is non empty Relation-like [: the carrier of n,NAT:] -defined the carrier of n -valued Function-like total V27([: the carrier of n,NAT:], the carrier of n) Element of bool [:[: the carrier of n,NAT:], the carrier of n:]
[: the carrier of n,NAT:] is non empty non trivial Relation-like non finite set
[:[: the carrier of n,NAT:], the carrier of n:] is non empty non trivial Relation-like non finite set
bool [:[: the carrier of n,NAT:], the carrier of n:] is non empty non trivial non finite set
L is Element of the carrier of n

() . (L,(x + f)) is Element of the carrier of n
[L,(x + f)] is set
() . [L,(x + f)] is set
() . (L,x) is Element of the carrier of n
[L,x] is set
() . [L,x] is set
() . (L,f) is Element of the carrier of n
[L,f] is set
() . [L,f] is set
(() . (L,x)) * (() . (L,f)) is Element of the carrier of n
the multF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . ((() . (L,x)),(() . (L,f))) is Element of the carrier of n
[(() . (L,x)),(() . (L,f))] is set
the multF of n . [(() . (L,x)),(() . (L,f))] is set

() . (L,(x + p)) is Element of the carrier of n
[L,(x + p)] is set
() . [L,(x + p)] is set
() . (L,p) is Element of the carrier of n
[L,p] is set
() . [L,p] is set
(() . (L,x)) * (() . (L,p)) is Element of the carrier of n
the multF of n . ((() . (L,x)),(() . (L,p))) is Element of the carrier of n
[(() . (L,x)),(() . (L,p))] is set
the multF of n . [(() . (L,x)),(() . (L,p))] is set

() . (L,(x + (p + 1))) is Element of the carrier of n
[L,(x + (p + 1))] is set
() . [L,(x + (p + 1))] is set

() . (L,((x + p) + 1)) is Element of the carrier of n
[L,((x + p) + 1)] is set
() . [L,((x + p) + 1)] is set
((() . (L,x)) * (() . (L,p))) * L is Element of the carrier of n
the multF of n . (((() . (L,x)) * (() . (L,p))),L) is Element of the carrier of n
[((() . (L,x)) * (() . (L,p))),L] is set
the multF of n . [((() . (L,x)) * (() . (L,p))),L] is set
(() . (L,p)) * L is Element of the carrier of n
the multF of n . ((() . (L,p)),L) is Element of the carrier of n
[(() . (L,p)),L] is set
the multF of n . [(() . (L,p)),L] is set
(() . (L,x)) * ((() . (L,p)) * L) is Element of the carrier of n
the multF of n . ((() . (L,x)),((() . (L,p)) * L)) is Element of the carrier of n
[(() . (L,x)),((() . (L,p)) * L)] is set
the multF of n . [(() . (L,x)),((() . (L,p)) * L)] is set
() . (L,(p + 1)) is Element of the carrier of n
[L,(p + 1)] is set
() . [L,(p + 1)] is set
(() . (L,x)) * (() . (L,(p + 1))) is Element of the carrier of n
the multF of n . ((() . (L,x)),(() . (L,(p + 1)))) is Element of the carrier of n
[(() . (L,x)),(() . (L,(p + 1)))] is set
the multF of n . [(() . (L,x)),(() . (L,(p + 1)))] is set

() . (L,(x + 0)) is Element of the carrier of n
[L,(x + 0)] is set
() . [L,(x + 0)] is set
1_ n is Element of the carrier of n
(() . (L,x)) * (1_ n) is Element of the carrier of n
the multF of n . ((() . (L,x)),(1_ n)) is Element of the carrier of n
[(() . (L,x)),(1_ n)] is set
the multF of n . [(() . (L,x)),(1_ n)] is set
() . (L,0) is Element of the carrier of n
[L,0] is set
() . [L,0] is set
(() . (L,x)) * (() . (L,0)) is Element of the carrier of n
the multF of n . ((() . (L,x)),(() . (L,0))) is Element of the carrier of n
[(() . (L,x)),(() . (L,0))] is set
the multF of n . [(() . (L,x)),(() . (L,0))] is set

n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set
L is finite Element of bool n
x is Element of n
{x} is non empty trivial finite 1 -element set
{x} \/ L is non empty finite set

p is set

the carrier of n is non empty set
0. n is V80(n) Element of the carrier of n

Sum L is Element of the carrier of n

L /. x is Element of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of n:] is non empty non trivial non finite set

f is non empty Relation-like NAT -defined the carrier of n -valued Function-like total V27( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
f . (len L) is Element of the carrier of n
f . 0 is Element of the carrier of n

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= q ) } is set

f . p9 is Element of the carrier of n

f . (p9 + 1) is Element of the carrier of n
L . (p9 + 1) is set
L /. (p9 + 1) is Element of the carrier of n
(0. n) + (L /. (p9 + 1)) is Element of the carrier of n
the addF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the addF of n . ((0. n),(L /. (p9 + 1))) is Element of the carrier of n
[(0. n),(L /. (p9 + 1))] is set
the addF of n . [(0. n),(L /. (p9 + 1))] is set

L . (p9 + 1) is set
L /. (p9 + 1) is Element of the carrier of n
(0. n) + (L /. (p9 + 1)) is Element of the carrier of n
the addF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the addF of n . ((0. n),(L /. (p9 + 1))) is Element of the carrier of n
[(0. n),(L /. (p9 + 1))] is set
the addF of n . [(0. n),(L /. (p9 + 1))] is set

L . (p9 + 1) is set
L /. (p9 + 1) is Element of the carrier of n
(L /. x) + (L /. (p9 + 1)) is Element of the carrier of n
the addF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the addF of n . ((L /. x),(L /. (p9 + 1))) is Element of the carrier of n
[(L /. x),(L /. (p9 + 1))] is set
the addF of n . [(L /. x),(L /. (p9 + 1))] is set
(L /. x) + (0. n) is Element of the carrier of n
the addF of n . ((L /. x),(0. n)) is Element of the carrier of n
[(L /. x),(0. n)] is set
the addF of n . [(L /. x),(0. n)] is set

the carrier of n is non empty set
0. n is V80(n) Element of the carrier of n

Product L is Element of the carrier of n

L /. x is Element of the carrier of n

Product p is Element of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of n:] is non empty non trivial non finite set
p . 1 is set
the multF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n "**" p is Element of the carrier of n

p /. 1 is Element of the carrier of n
q is non empty Relation-like NAT -defined the carrier of n -valued Function-like total V27( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
q . 1 is Element of the carrier of n
q . (len p) is Element of the carrier of n

p /. q is Element of the carrier of n

p . (len p) is set

p /. (len p) is Element of the carrier of n
<*(p /. (len p))*> is non empty trivial Relation-like NAT -defined the carrier of n -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support M9( the carrier of n,K256( the carrier of n))
K256( the carrier of n) is non empty functional FinSequence-membered M8( the carrier of n)

Product q is Element of the carrier of n
() * (0. n) is Element of the carrier of n
the multF of n . ((),(0. n)) is Element of the carrier of n
[(),(0. n)] is set
the multF of n . [(),(0. n)] is set

p /. p9 is Element of the carrier of n

p /. p9 is Element of the carrier of n

(p | f) . p9 is set
p . p9 is set
q . p9 is set
q /. p9 is Element of the carrier of n
Product q is Element of the carrier of n
() * (p /. (len p)) is Element of the carrier of n
the multF of n . ((),(p /. (len p))) is Element of the carrier of n
[(),(p /. (len p))] is set
the multF of n . [(),(p /. (len p))] is set
(0. n) * (p /. (len p)) is Element of the carrier of n
the multF of n . ((0. n),(p /. (len p))) is Element of the carrier of n
[(0. n),(p /. (len p))] is set
the multF of n . [(0. n),(p /. (len p))] is set

p /. q is Element of the carrier of n
Product p is Element of the carrier of n

Product f is Element of the carrier of n

f /. p is Element of the carrier of n

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

Sum f 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 addF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the addF of n . (L,(Sum x)) is Element of the carrier of n
[L,(Sum x)] is set
the addF of n . [L,(Sum x)] is set

f /. p is Element of the carrier of n
x /. p is Element of the carrier of n
L + (x /. p) is Element of the carrier of n
the addF of n . (L,(x /. p)) is Element of the carrier of n
[L,(x /. p)] is set
the addF of n . [L,(x /. p)] is set

f /. p is Element of the carrier of n
x /. p is Element of the carrier of n
L + (x /. p) is Element of the carrier of n
the addF of n . (L,(x /. p)) is Element of the carrier of n
[L,(x /. p)] is set
the addF of n . [L,(x /. p)] is set
[:NAT, the carrier of n:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of n:] is non empty non trivial non finite set
0. n is V80(n) Element of the carrier of n
q is non empty Relation-like NAT -defined the carrier of n -valued Function-like total V27( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
q . (len f) is Element of the carrier of n
q . 0 is Element of the carrier of n

Seg p9 is finite p9 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= p9 ) } is set

Seg q9 is finite q9 -element Element of bool NAT
p9 is non empty Relation-like NAT -defined the carrier of n -valued Function-like total V27( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
p9 . (len x) is Element of the carrier of n
p9 . 0 is Element of the carrier of n

p9 . bg is Element of the carrier of n
q . bg is Element of the carrier of n
L + (p9 . bg) is Element of the carrier of n
the addF of n . (L,(p9 . bg)) is Element of the carrier of n
[L,(p9 . bg)] is set
the addF of n . [L,(p9 . bg)] is set

p9 . (bg + 1) is Element of the carrier of n
q . (bg + 1) is Element of the carrier of n
L + (p9 . (bg + 1)) is Element of the carrier of n
the addF of n . (L,(p9 . (bg + 1))) is Element of the carrier of n
[L,(p9 . (bg + 1))] is set
the addF of n . [L,(p9 . (bg + 1))] is set
x . (bg + 1) is set
x /. (bg + 1) is Element of the carrier of n
f . (bg + 1) is set
f /. (bg + 1) is Element of the carrier of n
L + (x /. (bg + 1)) is Element of the carrier of n
the addF of n . (L,(x /. (bg + 1))) is Element of the carrier of n
[L,(x /. (bg + 1))] is set
the addF of n . [L,(x /. (bg + 1))] is set
(q . bg) + (L + (x /. (bg + 1))) is Element of the carrier of n
the addF of n . ((q . bg),(L + (x /. (bg + 1)))) is Element of the carrier of n
[(q . bg),(L + (x /. (bg + 1)))] is set
the addF of n . [(q . bg),(L + (x /. (bg + 1)))] is set
(q . bg) + (x /. (bg + 1)) is Element of the carrier of n
the addF of n . ((q . bg),(x /. (bg + 1))) is Element of the carrier of n
[(q . bg),(x /. (bg + 1))] is set
the addF of n . [(q . bg),(x /. (bg + 1))] is set
L + ((q . bg) + (x /. (bg + 1))) is Element of the carrier of n
the addF of n . (L,((q . bg) + (x /. (bg + 1)))) is Element of the carrier of n
[L,((q . bg) + (x /. (bg + 1)))] is set
the addF of n . [L,((q . bg) + (x /. (bg + 1)))] is set

x . (bg + 1) is set
x /. (bg + 1) is Element of the carrier of n
f . (bg + 1) is set
f /. (bg + 1) is Element of the carrier of n
(q . bg) + (f /. (bg + 1)) is Element of the carrier of n
the addF of n . ((q . bg),(f /. (bg + 1))) is Element of the carrier of n
[(q . bg),(f /. (bg + 1))] is set
the addF of n . [(q . bg),(f /. (bg + 1))] is set

x . (bg + 1) is set
x /. (bg + 1) is Element of the carrier of n
f . (bg + 1) is set
f /. (bg + 1) is Element of the carrier of n
(q . bg) + (f /. (bg + 1)) is Element of the carrier of n
the addF of n . ((q . bg),(f /. (bg + 1))) is Element of the carrier of n
[(q . bg),(f /. (bg + 1))] is set
the addF of n . [(q . bg),(f /. (bg + 1))] is set
(L + (p9 . bg)) + (x /. (bg + 1)) is Element of the carrier of n
the addF of n . ((L + (p9 . bg)),(x /. (bg + 1))) is Element of the carrier of n
[(L + (p9 . bg)),(x /. (bg + 1))] is set
the addF of n . [(L + (p9 . bg)),(x /. (bg + 1))] is set
(p9 . bg) + (x /. (bg + 1)) is Element of the carrier of n
the addF of n . ((p9 . bg),(x /. (bg + 1))) is Element of the carrier of n
[(p9 . bg),(x /. (bg + 1))] is set
the addF of n . [(p9 . bg),(x /. (bg + 1))] is set
L + ((p9 . bg) + (x /. (bg + 1))) is Element of the carrier of n
the addF of n . (L,((p9 . bg) + (x /. (bg + 1)))) is Element of the carrier of n
[L,((p9 . bg) + (x /. (bg + 1)))] is set
the addF of n . [L,((p9 . bg) + (x /. (bg + 1)))] is set
L + (p9 . 0) is Element of the carrier of n
the addF of n . (L,(p9 . 0)) is Element of the carrier of n
[L,(p9 . 0)] is set
the addF of n . [L,(p9 . 0)] is set

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

Product f is Element of the carrier of n
Product x is Element of the carrier of n
L * () is Element of the carrier of n
the multF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n . (L,()) is Element of the carrier of n
[L,()] is set
the multF of n . [L,()] is set

f /. p is Element of the carrier of n
x /. p is Element of the carrier of n
L * (x /. p) is Element of the carrier of n
the multF of n . (L,(x /. p)) is Element of the carrier of n
[L,(x /. p)] is set
the multF of n . [L,(x /. p)] is set

f /. p is Element of the carrier of n
x /. p is Element of the carrier of n
L * (x /. p) is Element of the carrier of n
the multF of n . (L,(x /. p)) is Element of the carrier of n
[L,(x /. p)] is set
the multF of n . [L,(x /. p)] is set
the multF of n "**" x is Element of the carrier of n
the multF of n "**" f is Element of the carrier of n

[:NAT, the carrier of n:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of n:] is non empty non trivial non finite set
x . 1 is set
p9 is non empty Relation-like NAT -defined the carrier of n -valued Function-like total V27( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
p9 . 1 is Element of the carrier of n
p9 . (len x) is Element of the carrier of n
f . 1 is set
q9 is non empty Relation-like NAT -defined the carrier of n -valued Function-like total V27( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
q9 . 1 is Element of the carrier of n
q9 . (len x) is Element of the carrier of n

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= p ) } is set

p9 . bg is Element of the carrier of n
q9 . bg is Element of the carrier of n
L * (p9 . bg) is Element of the carrier of n
the multF of n . (L,(p9 . bg)) is Element of the carrier of n
[L,(p9 . bg)] is set
the multF of n . [L,(p9 . bg)] is set

p9 . (bg + 1) is Element of the carrier of n
q9 . (bg + 1) is Element of the carrier of n
L * (p9 . (bg + 1)) is Element of the carrier of n
the multF of n . (L,(p9 . (bg + 1))) is Element of the carrier of n
[L,(p9 . (bg + 1))] is set
the multF of n . [L,(p9 . (bg + 1))] is set
x . (bg + 1) is set
x /. (bg + 1) is Element of the carrier of n
f . (bg + 1) is set
f /. (bg + 1) is Element of the carrier of n
L * (x /. (bg + 1)) is Element of the carrier of n
the multF of n . (L,(x /. (bg + 1))) is Element of the carrier of n
[L,(x /. (bg + 1))] is set
the multF of n . [L,(x /. (bg + 1))] is set
(p9 . bg) * (L * (x /. (bg + 1))) is Element of the carrier of n
the multF of n . ((p9 . bg),(L * (x /. (bg + 1)))) is Element of the carrier of n
[(p9 . bg),(L * (x /. (bg + 1)))] is set
the multF of n . [(p9 . bg),(L * (x /. (bg + 1)))] is set
(p9 . bg) * (x /. (bg + 1)) is Element of the carrier of n
the multF of n . ((p9 . bg),(x /. (bg + 1))) is Element of the carrier of n
[(p9 . bg),(x /. (bg + 1))] is set
the multF of n . [(p9 . bg),(x /. (bg + 1))] is set
((p9 . bg) * (x /. (bg + 1))) * L is Element of the carrier of n
the multF of n . (((p9 . bg) * (x /. (bg + 1))),L) is Element of the carrier of n
[((p9 . bg) * (x /. (bg + 1))),L] is set
the multF of n . [((p9 . bg) * (x /. (bg + 1))),L] is set
(p9 . (bg + 1)) * L is Element of the carrier of n
the multF of n . ((p9 . (bg + 1)),L) is Element of the carrier of n
[(p9 . (bg + 1)),L] is set
the multF of n . [(p9 . (bg + 1)),L] is set

x . (bg + 1) is set
x /. (bg + 1) is Element of the carrier of n
f . (bg + 1) is set
f /. (bg + 1) is Element of the carrier of n
(q9 . bg) * (f /. (bg + 1)) is Element of the carrier of n
the multF of n . ((q9 . bg),(f /. (bg + 1))) is Element of the carrier of n
[(q9 . bg),(f /. (bg + 1))] is set
the multF of n . [(q9 . bg),(f /. (bg + 1))] is set
the multF of n . ((q9 . bg),(x . (bg + 1))) is set
[(q9 . bg),(x . (bg + 1))] is set
the multF of n . [(q9 . bg),(x . (bg + 1))] is set

x . (bg + 1) is set
x /. (bg + 1) is Element of the carrier of n
f . (bg + 1) is set
f /. (bg + 1) is Element of the carrier of n
(q9 . bg) * (f /. (bg + 1)) is Element of the carrier of n
the multF of n . ((q9 . bg),(f /. (bg + 1))) is Element of the carrier of n
[(q9 . bg),(f /. (bg + 1))] is set
the multF of n . [(q9 . bg),(f /. (bg + 1))] is set
(L * (p9 . bg)) * (x /. (bg + 1)) is Element of the carrier of n
the multF of n . ((L * (p9 . bg)),(x /. (bg + 1))) is Element of the carrier of n
[(L * (p9 . bg)),(x /. (bg + 1))] is set
the multF of n . [(L * (p9 . bg)),(x /. (bg + 1))] is set
(p9 . bg) * (x /. (bg + 1)) is Element of the carrier of n
the multF of n . ((p9 . bg),(x /. (bg + 1))) is Element of the carrier of n
[(p9 . bg),(x /. (bg + 1))] is set
the multF of n . [(p9 . bg),(x /. (bg + 1))] is set
L * ((p9 . bg) * (x /. (bg + 1))) is Element of the carrier of n
the multF of n . (L,((p9 . bg) * (x /. (bg + 1)))) is Element of the carrier of n
[L,((p9 . bg) * (x /. (bg + 1)))] is set
the multF of n . [L,((p9 . bg) * (x /. (bg + 1)))] is set
x /. 1 is Element of the carrier of n
f /. 1 is Element of the carrier of n

x /. 1 is Element of the carrier of n
L * (x /. 1) is Element of the carrier of n
the multF of n . (L,(x /. 1)) is Element of the carrier of n
[L,(x /. 1)] is set
the multF of n . [L,(x /. 1)] is set
L * (p9 . 1) is Element of the carrier of n
the multF of n . (L,(p9 . 1)) is Element of the carrier of n
[L,(p9 . 1)] is set
the multF of n . [L,(p9 . 1)] is set
L * (p9 . 1) is Element of the carrier of n
the multF of n . (L,(p9 . 1)) is Element of the carrier of n
[L,(p9 . 1)] is set
the multF of n . [L,(p9 . 1)] is set
L * (p9 . 1) is Element of the carrier of n
the multF of n . (L,(p9 . 1)) is Element of the carrier of n
[L,(p9 . 1)] is set
the multF of n . [L,(p9 . 1)] is set

n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set

rng (SgmX (x,L)) is finite set
n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set
L is finite Element of bool n

dom (SgmX (x,L)) is finite Element of bool NAT

(SgmX (x,L)) /. f is Element of n
(SgmX (x,L)) /. p is Element of n
n is set

n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set
L is finite Element of bool n
x is Element of n
{x} is non empty trivial finite 1 -element set
{x} \/ L is non empty finite set
f is finite Element of bool n

dom (SgmX (p,f)) is finite Element of bool NAT

field p is set
dom (SgmX (p,L)) is finite Element of bool NAT

Seg q9 is finite q9 -element Element of bool NAT

(len (SgmX (p,L))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real positive non negative Element of NAT

(SgmX (p,f)) /. bg is Element of n
bg - 1 is V11() V12() V45() ext-real Element of REAL
Seg (len (SgmX (p,f))) is finite len (SgmX (p,f)) -element Element of bool NAT
1 - 1 is V11() V12() V45() ext-real Element of REAL

(SgmX (p,f)) /. (p9 + 1) is Element of n
(SgmX (p,L)) /. (p9 + 1) is Element of n
(SgmX (p,f)) . (p9 + 1) is set
rng (SgmX (p,f)) is finite set
rng (SgmX (p,L)) is finite set
p9 is set
(SgmX (p,L)) . p9 is set

(SgmX (p,f)) /. m is Element of n
(SgmX (p,L)) /. m is Element of n
(SgmX (p,L)) . (p9 + 1) is set
m is set
(SgmX (p,f)) . m is set
(SgmX (p,L)) /. m is Element of n
[((SgmX (p,L)) /. (p9 + 1)),((SgmX (p,L)) /. m)] is set

(SgmX (p,f)) /. m is Element of n
[((SgmX (p,f)) /. m),((SgmX (p,L)) /. m)] is set
[((SgmX (p,f)) /. m),((SgmX (p,f)) /. (p9 + 1))] is set
(SgmX (p,f)) . m is set
(SgmX (p,L)) /. m is Element of n
[((SgmX (p,f)) /. (p9 + 1)),((SgmX (p,f)) /. m)] is set

(SgmX (p,f)) /. p9 is Element of n
(SgmX (p,L)) /. p9 is Element of n
(SgmX (p,f)) /. 1 is Element of n
(SgmX (p,L)) /. 1 is Element of n
(SgmX (p,f)) . 1 is set
rng (SgmX (p,f)) is finite set
rng (SgmX (p,L)) is finite set
p9 is set
(SgmX (p,L)) . p9 is set
(SgmX (p,L)) . 1 is set

(SgmX (p,L)) /. m is Element of n
[((SgmX (p,L)) /. 1),((SgmX (p,L)) /. m)] is set
[((SgmX (p,L)) /. 1),((SgmX (p,f)) /. 1)] is set
m is set
(SgmX (p,f)) . m is set

(SgmX (p,f)) /. m is Element of n
[((SgmX (p,f)) /. 1),((SgmX (p,f)) /. m)] is set
[((SgmX (p,f)) /. 1),((SgmX (p,L)) /. 1)] is set
n is set
bool n is non empty set
[:n,n:] is Relation-like set
bool [:n,n:] is non empty set
L is finite Element of bool n
x is Element of n
{x} is non empty trivial finite 1 -element set
{x} \/ L is non empty finite set
f is finite Element of bool n

dom (SgmX (p,f)) is finite Element of bool NAT

field p is set
dom (SgmX (p,L)) is finite Element of bool NAT

Seg q9 is finite q9 -element Element of bool NAT

(SgmX (p,f)) /. q is Element of n

Seg (len (SgmX (p,f))) is finite len (SgmX (p,f)) -element Element of bool NAT
1 - 1 is V11() V12() V45() ext-real Element of REAL
q - 1 is V11() V12() V45() ext-real Element of REAL

(len (SgmX (p,L))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real positive non negative Element of NAT

(SgmX (p,f)) /. ((p9 + 1) + 1) is Element of n
(SgmX (p,L)) /. (p9 + 1) is Element of n

(SgmX (p,f)) /. (p9 + 2) is Element of n
(SgmX (p,f)) . (p9 + 2) is set
rng (SgmX (p,f)) is finite set
rng (SgmX (p,L)) is finite set
p9 is set
(SgmX (p,L)) . p9 is set

(SgmX (p,L)) /. m is Element of n
(SgmX (p,L)) . m is set
(SgmX (p,L)) . (p9 + 1) is set

(SgmX (p,f)) /. (m + 1) is Element of n
(SgmX (p,f)) /. m is Element of n

(SgmX (p,f)) /. m is Element of n
(SgmX (p,L)) /. m is Element of n
m - 1 is V11() V12() V45() ext-real Element of REAL
(p9 + 1) - 1 is V11() V12() V45() ext-real Element of REAL
(m - 1) + 1 is V11() V12() V45() ext-real Element of REAL

(SgmX (p,L)) /. (m - 1) is Element of n
m is set
(SgmX (p,f)) . m is set

(SgmX (p,f)) /. m is Element of n
(SgmX (p,f)) . m is set
Seg (len (SgmX (p,L))) is finite len (SgmX (p,L)) -element Element of bool NAT
[((SgmX (p,L)) /. (p9 + 1)),((SgmX (p,L)) /. m)] is set
[((SgmX (p,L)) /. m),((SgmX (p,L)) /. (p9 + 1))] is set

(SgmX (p,f)) /. (p9 + 1) is Element of n
(SgmX (p,L)) /. p9 is Element of n

(SgmX (p,f)) /. (q + 1) is Element of n
(SgmX (p,L)) /. q is Element of n
(SgmX (p,L)) . q is set
rng (SgmX (p,L)) is finite set
rng (SgmX (p,f)) is finite set
p9 is set
(SgmX (p,f)) . p9 is set

(SgmX (p,f)) /. m is Element of n
(SgmX (p,f)) . m is set
(SgmX (p,L)) /. m is Element of n
[((SgmX (p,f)) /. (q + 1)),((SgmX (p,f)) /. m)] is set
(SgmX (p,f)) . (q + 1) is set
m is set
(SgmX (p,L)) . m is set

(SgmX (p,L)) /. m is Element of n
(SgmX (p,L)) . m is set
(SgmX (p,f)) /. m is Element of n
[((SgmX (p,f)) /. m),((SgmX (p,f)) /. (q + 1))] is set
n is non empty set
bool n is non empty set
[:n,n:] is non empty Relation-like set
bool [:n,n:] is non empty set
L is finite Element of bool n
x is Element of n
{x} is non empty trivial finite 1 -element set
{x} \/ L is non empty finite set
f is finite Element of bool n

dom (SgmX (p,f)) is finite Element of bool NAT

(SgmX (p,f)) /. (q + 1) is Element of n

Seg (len (SgmX (p,f))) is finite len (SgmX (p,f)) -element Element of bool NAT
(q + 1) - 1 is V11() V12() V45() ext-real Element of REAL
(len (SgmX (p,f))) - 1 is V11() V12() V45() ext-real Element of REAL

(len (SgmX (p,L))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real positive non negative Element of NAT
len (Ins ((SgmX (p,L)),q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT
Seg (len (Ins ((SgmX (p,L)),q,x))) is finite len (Ins ((SgmX (p,L)),q,x)) -element Element of bool NAT
dom (Ins ((SgmX (p,L)),q,x)) is finite Element of bool NAT

(SgmX (p,f)) . p is set
(Ins ((SgmX (p,L)),q,x)) . p is set
(SgmX (p,f)) /. p is Element of n
(Ins ((SgmX (p,L)),q,x)) /. (q + 1) is Element of n

[:NAT,n:] is non empty non trivial Relation-like non finite set
bool [:NAT,n:] is non empty non trivial non finite set
dom ((SgmX (p,L)) | (Seg q)) is finite Element of bool NAT

dom ((SgmX (p,L)) | q) is finite Element of bool NAT
(SgmX (p,f)) /. p is Element of n
(SgmX (p,L)) /. p is Element of n
(Ins ((SgmX (p,L)),q,x)) /. p is Element of n
1 - 1 is V11() V12() V45() ext-real Element of REAL
p - 1 is V11() V12() V45() ext-real Element of REAL

(SgmX (p,f)) /. (q + 1) is Element of n
(SgmX (p,L)) /. q is Element of n
(Ins ((SgmX (p,L)),q,x)) /. (q + 1) is Element of n
n is set

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

dom () is Element of bool n
bool n is non empty set
x is set

dom L is Element of bool n
n is set

bool [:n,NAT:] is non empty set

x is set
rng L is V221() V222() V223() V224() V226() set
f is set
p is set
[f,p] is set
dom L is Element of bool n
bool n is non empty set
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 non empty functional Element of bool (Bags n)
bool (Bags n) is non empty set
() +* ( the Element of n,1) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() 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 epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() V46() ext-real non negative Element of NAT

{ the Element of n} is non empty trivial