:: POLYNOM2 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal 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

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is Relation-like set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is Relation-like set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is Relation-like set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is Relation-like set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty non trivial Relation-like non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

K266() is set

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

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() Function-yielding V48() ext-real non positive non negative V211() V212() V213() V214() FinSequence-yielding finite-support 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())

K633() is non empty strict unital associative commutative multMagma

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real positive non negative Element of NAT

[:NAT,REAL:] is Relation-like set

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

K662() is Relation-like NAT -defined Function-like total set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real positive non negative Element of NAT

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

dom {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() Function-yielding V48() ext-real non positive non negative V211() V212() V213() V214() FinSequence-yielding finite-support set

rng {} is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() Function-yielding V48() V60() ext-real non positive non negative V211() V212() V213() V214() V215() V216() V217() V218() V221() V222() V223() V224() V226() FinSequence-yielding finite-support set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() Function-yielding V48() ext-real non positive non negative V211() V212() V213() V214() FinSequence-yielding finite-support Element of NAT

card {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() Function-yielding V48() ext-real non positive non negative V211() V212() V213() V214() FinSequence-yielding finite-support set

Bags {} is non empty functional Element of bool (Bags {})

Bags {} is non empty set

bool (Bags {}) 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

x is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,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

x is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,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

x is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,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

x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

x + f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(power n) . (L,(x + f)) is Element of the carrier of n

[L,(x + f)] is set

(power n) . [L,(x + f)] is set

(power n) . (L,x) is Element of the carrier of n

[L,x] is set

(power n) . [L,x] is set

(power n) . (L,f) is Element of the carrier of n

[L,f] is set

(power n) . [L,f] is set

((power n) . (L,x)) * ((power n) . (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 . (((power n) . (L,x)),((power n) . (L,f))) is Element of the carrier of n

[((power n) . (L,x)),((power n) . (L,f))] is set

the multF of n . [((power n) . (L,x)),((power n) . (L,f))] is set

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

x + p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(power n) . (L,(x + p)) is Element of the carrier of n

[L,(x + p)] is set

(power n) . [L,(x + p)] is set

(power n) . (L,p) is Element of the carrier of n

[L,p] is set

(power n) . [L,p] is set

((power n) . (L,x)) * ((power n) . (L,p)) is Element of the carrier of n

the multF of n . (((power n) . (L,x)),((power n) . (L,p))) is Element of the carrier of n

[((power n) . (L,x)),((power n) . (L,p))] is set

the multF of n . [((power n) . (L,x)),((power n) . (L,p))] is set

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

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

(power n) . (L,(x + (p + 1))) is Element of the carrier of n

[L,(x + (p + 1))] is set

(power n) . [L,(x + (p + 1))] is set

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

(power n) . (L,((x + p) + 1)) is Element of the carrier of n

[L,((x + p) + 1)] is set

(power n) . [L,((x + p) + 1)] is set

(((power n) . (L,x)) * ((power n) . (L,p))) * L is Element of the carrier of n

the multF of n . ((((power n) . (L,x)) * ((power n) . (L,p))),L) is Element of the carrier of n

[(((power n) . (L,x)) * ((power n) . (L,p))),L] is set

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

((power n) . (L,p)) * L is Element of the carrier of n

the multF of n . (((power n) . (L,p)),L) is Element of the carrier of n

[((power n) . (L,p)),L] is set

the multF of n . [((power n) . (L,p)),L] is set

((power n) . (L,x)) * (((power n) . (L,p)) * L) is Element of the carrier of n

the multF of n . (((power n) . (L,x)),(((power n) . (L,p)) * L)) is Element of the carrier of n

[((power n) . (L,x)),(((power n) . (L,p)) * L)] is set

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

(power n) . (L,(p + 1)) is Element of the carrier of n

[L,(p + 1)] is set

(power n) . [L,(p + 1)] is set

((power n) . (L,x)) * ((power n) . (L,(p + 1))) is Element of the carrier of n

the multF of n . (((power n) . (L,x)),((power n) . (L,(p + 1)))) is Element of the carrier of n

[((power n) . (L,x)),((power n) . (L,(p + 1)))] is set

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

x + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(power n) . (L,(x + 0)) is Element of the carrier of n

[L,(x + 0)] is set

(power n) . [L,(x + 0)] is set

1_ n is Element of the carrier of n

((power n) . (L,x)) * (1_ n) is Element of the carrier of n

the multF of n . (((power n) . (L,x)),(1_ n)) is Element of the carrier of n

[((power n) . (L,x)),(1_ n)] is set

the multF of n . [((power n) . (L,x)),(1_ n)] is set

(power n) . (L,0) is Element of the carrier of n

[L,0] is set

(power n) . [L,0] is set

((power n) . (L,x)) * ((power n) . (L,0)) is Element of the carrier of n

the multF of n . (((power n) . (L,x)),((power n) . (L,0))) is Element of the carrier of n

[((power n) . (L,x)),((power n) . (L,0))] is set

the multF of n . [((power n) . (L,x)),((power n) . (L,0))] is set

F_Real is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

dom n is finite Element of bool NAT

L is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg f is finite f -element Element of bool NAT

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 Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,n:]

p is set

n is non empty right_zeroed left_zeroed addLoopStr

the carrier of n is non empty set

0. n is V80(n) Element of the carrier of n

L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

dom L is finite Element of bool NAT

Sum L is Element of the carrier of n

x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

len L is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg p is finite p -element Element of bool NAT

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

{ b

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

f . p9 is Element of the carrier of n

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

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

q9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

Seg q is finite q -element Element of bool NAT

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

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

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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

n is non empty left_add-cancelable right_add-cancelable right_complementable unital add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of n is non empty set

0. n is V80(n) Element of the carrier of n

L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

dom L is finite Element of bool NAT

Product L is Element of the carrier of n

x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

L /. x is Element of the carrier of n

f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

p is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

dom p is finite Element of bool NAT

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

Seg (len p) is finite len p -element Element of bool NAT

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

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p /. q is Element of the carrier of n

Seg f is finite f -element Element of bool NAT

p | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined the carrier of n -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT, the carrier of n:]

q 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 q is finite Element of bool NAT

p . (len p) is set

<*(p . (len p))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set

q ^ <*(p . (len p))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support 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)

q ^ <*(p /. (len p))*> is non empty Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

Product q is Element of the carrier of n

(Product q) * (0. n) is Element of the carrier of n

the multF of n . ((Product q),(0. n)) is Element of the carrier of n

[(Product q),(0. n)] is set

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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p /. p9 is Element of the carrier of n

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p /. p9 is Element of the carrier of n

p | f 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

(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

(Product q) * (p /. (len p)) is Element of the carrier of n

the multF of n . ((Product q),(p /. (len p))) is Element of the carrier of n

[(Product q),(p /. (len p))] is set

the multF of n . [(Product q),(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 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

dom p is finite Element of bool NAT

p /. q is Element of the carrier of n

Product p is Element of the carrier of n

len L is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

f is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

dom f is finite Element of bool NAT

Product f is Element of the carrier of n

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

f /. p is Element of the carrier of n

f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

n is non empty Abelian add-associative addLoopStr

the carrier of n is non empty set

L is Element of the carrier of n

x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

f is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

dom x is finite Element of bool NAT

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

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg p9 is finite p9 -element Element of bool NAT

{ b

dom f is finite Element of bool NAT

q9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative 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

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

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

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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

Seg p is finite p -element Element of bool NAT

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

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

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

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

n is non empty associative commutative doubleLoopStr

the carrier of n is non empty set

L is Element of the carrier of n

x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

f is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

dom x is finite Element of bool NAT

Product f is Element of the carrier of n

Product x is Element of the carrier of n

L * (Product x) 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,(Product x)) is Element of the carrier of n

[L,(Product x)] is set

the multF of n . [L,(Product x)] is set

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

dom f is finite Element of bool NAT

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg q is finite q -element Element of bool NAT

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

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg p is finite p -element Element of bool NAT

{ b

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

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

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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

Seg q is finite q -element Element of bool NAT

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

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

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

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

n is set

bool n is non empty set

[:n,n:] is Relation-like set

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

L is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() Function-yielding V48() ext-real non positive non negative V211() V212() V213() V214() FinSequence-yielding finite-support Element of bool n

x is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,n:]

SgmX (x,L) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

x is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,n:]

SgmX (x,L) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

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

n is set

L is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

dom L is finite Element of bool NAT

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

p is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,n:]

SgmX (p,f) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

SgmX (p,L) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

field p is set

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

q9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg q9 is finite q9 -element Element of bool NAT

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg p is finite p -element Element of bool NAT

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

card f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

card L is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(card 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 (SgmX (p,L)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of 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

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real 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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

bg + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p9 + 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) 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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

p is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,n:]

SgmX (p,f) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

SgmX (p,L) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

field p is set

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

q9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg q9 is finite q9 -element Element of bool NAT

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

Seg p is finite p -element Element of bool NAT

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

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

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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

q + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

card f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

card L is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

bg is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

(p9 + 1) + 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

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

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

p9 + 2 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 + 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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(SgmX (p,L)) /. m is Element of n

(SgmX (p,L)) . m is set

(SgmX (p,L)) . (p9 + 1) is set

m + 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)) /. (m + 1) is Element of n

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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

m + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

m is set

(SgmX (p,f)) . m is set

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

p9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

p9 + 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) is Element of n

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

q + 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)) /. (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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

p is Relation-like n -defined n -valued total V27(n,n) reflexive antisymmetric transitive Element of bool [:n,n:]

SgmX (p,f) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

SgmX (p,L) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

q + 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)) /. (q + 1) is Element of n

Ins ((SgmX (p,L)),q,x) is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

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

q + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

card f is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

card L is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(card 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 (SgmX (p,L)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of 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

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

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative set

(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

Seg q is finite q -element Element of bool NAT

(SgmX (p,L)) | (Seg q) is Relation-like NAT -defined Seg q -defined NAT -defined n -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,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

(SgmX (p,L)) | q is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n

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

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

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

p + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT

(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

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags 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

L is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

support L is finite set

dom (EmptyBag n) is Element of bool n

bool n is non empty set

x is set

L . x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() V46() ext-real non negative Element of NAT

(EmptyBag n) . x is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() V46() ext-real non negative Element of NAT

dom L is Element of bool n

n is set

[:n,NAT:] is Relation-like set

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

L is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support 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

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags 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

(EmptyBag n) +* ( the Element of n,1) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

dom (EmptyBag n) is Element of bool n

bool n is non empty set

((EmptyBag n) +* ( 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 .--> 1 is Relation-like n -defined { the Element of n} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one finite V211() V212() V213() V214() finite-support set

{ the Element of n} is non empty trivial