:: 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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= q ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= p9 ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() finite cardinal V45() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
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