:: FINSEQ_3 semantic presentation

REAL is set

NAT is non empty non trivial V15() V16() V17() V18() non finite cardinal limit_cardinal countable denumerable Element of K27(REAL)

K27(REAL) is non empty set

NAT is non empty non trivial V15() V16() V17() V18() non finite cardinal limit_cardinal countable denumerable set

K27(NAT) is non empty non trivial non finite set

K27(NAT) is non empty non trivial non finite set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set

1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{{},1} is non empty finite V40() countable set

K28(1,1) is Relation-like non empty finite countable set

K27(K28(1,1)) is non empty finite V40() countable set

K28(K28(1,1),1) is Relation-like non empty finite countable set

K27(K28(K28(1,1),1)) is non empty finite V40() countable set

2 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

3 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of NAT

card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set

Seg 1 is non empty trivial finite 1 -element countable Element of K27(NAT)

{1} is non empty trivial finite V40() 1 -element countable set

Seg 2 is non empty finite 2 -element countable Element of K27(NAT)

{1,2} is non empty finite V40() countable set

dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set

rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable with_non-empty_elements set

INT is set

product {} is functional non empty finite with_common_domain product-like countable set

{{}} is functional non empty trivial finite V40() 1 -element with_common_domain countable set

SubFuncs {} is set

Seg 3 is non empty finite 3 -element countable Element of K27(NAT)

{1,2,3} is non empty finite countable set

2 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{(2 + 1)} is non empty trivial finite V40() 1 -element countable set

{1,2} \/ {(2 + 1)} is non empty finite V40() countable set

4 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg 4 is non empty finite 4 -element countable Element of K27(NAT)

{1,2,3,4} is non empty finite countable set

3 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{(3 + 1)} is non empty trivial finite V40() 1 -element countable set

{1,2,3} \/ {(3 + 1)} is non empty finite countable set

5 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg 5 is non empty finite 5 -element countable Element of K27(NAT)

{1,2,3,4,5} is non empty finite countable set

4 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{(4 + 1)} is non empty trivial finite V40() 1 -element countable set

{1,2,3,4} \/ {(4 + 1)} is non empty finite countable set

6 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg 6 is non empty finite 6 -element countable Element of K27(NAT)

{1,2,3,4,5,6} is non empty finite countable set

5 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{(5 + 1)} is non empty trivial finite V40() 1 -element countable set

{1,2,3,4,5} \/ {(5 + 1)} is non empty finite countable set

7 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg 7 is non empty finite 7 -element countable Element of K27(NAT)

{1,2,3,4,5,6,7} is non empty finite countable set

6 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{(6 + 1)} is non empty trivial finite V40() 1 -element countable set

{1,2,3,4,5,6} \/ {(6 + 1)} is non empty finite countable set

8 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg 8 is non empty finite 8 -element countable Element of K27(NAT)

{1,2,3,4,5,6,7,8} is non empty finite countable set

7 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{(7 + 1)} is non empty trivial finite V40() 1 -element countable set

{1,2,3,4,5,6,7} \/ {(7 + 1)} is non empty finite countable set

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg i is finite i -element countable Element of K27(NAT)

i + 0 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg (i + D) is finite i + D -element countable Element of K27(NAT)

0 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + 0 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i - x is ext-real V25() V26() V33() set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

x + n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i - D is ext-real V25() V26() V33() set

D - D is ext-real V25() V26() V33() set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

i + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

{(i + 1)} is non empty trivial finite V40() 1 -element countable set

(Seg i) /\ {(i + 1)} is finite countable Element of K27(NAT)

the Element of (Seg i) /\ {(i + 1)} is Element of (Seg i) /\ {(i + 1)}

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (i + 1) is non empty finite i + 1 -element countable Element of K27(NAT)

Seg i is finite i -element countable Element of K27(NAT)

(Seg (i + 1)) \ (Seg i) is finite countable Element of K27(NAT)

{(i + 1)} is non empty trivial finite V40() 1 -element countable set

(Seg i) \/ {(i + 1)} is non empty finite countable set

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

i + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (i + 1) is non empty finite i + 1 -element countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg (i + D) is finite i + D -element countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg (i + D) is finite i + D -element countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

i is set

{i} is non empty trivial finite 1 -element countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

i is set

D is set

{i,D} is non empty finite countable set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg x is finite x -element countable Element of K27(NAT)

1 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom i is finite countable Element of K27(NAT)

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

i ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom (i ^ D) is finite countable Element of K27(NAT)

x is set

D is set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom i is finite countable Element of K27(NAT)

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom i is finite countable Element of K27(NAT)

D is set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (len i) is finite len i -element countable Element of K27(NAT)

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom i is finite countable Element of K27(NAT)

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg (len i) is finite len i -element countable Element of K27(NAT)

Seg (len i) is finite len i -element countable Element of K27(NAT)

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom i is finite countable Element of K27(NAT)

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D - 1 is ext-real V25() V26() V33() set

(len i) - D is ext-real V25() V26() V33() set

0 + D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

0 + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom i is finite countable Element of K27(NAT)

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom D is finite countable Element of K27(NAT)

Seg (len i) is finite len i -element countable Element of K27(NAT)

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom i is finite countable Element of K27(NAT)

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom D is finite countable Element of K27(NAT)

Seg (len D) is finite len D -element countable Element of K27(NAT)

Seg (len i) is finite len i -element countable Element of K27(NAT)

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

rng i is finite countable set

dom i is finite countable Element of K27(NAT)

D is set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (len i) is finite len i -element countable Element of K27(NAT)

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

rng i is finite countable set

dom i is finite countable Element of K27(NAT)

the Element of rng i is Element of rng i

i is set

D is set

<*i,D*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

i is set

D is set

x is set

<*i,D,x*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

i is set

<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

D is set

x is set

<*D,x*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

len <*i*> is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i is set

<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

D is set

x is set

n is set

<*D,x,n*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

len <*i*> is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i is set

D is set

<*i,D*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

x is set

n is set

m9 is set

<*x,n,m9*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like countable set

len <*i,D*> is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom D is finite countable Element of K27(NAT)

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len D) + (len x) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom x is finite countable Element of K27(NAT)

D ^ x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom i is finite countable Element of K27(NAT)

Seg ((len D) + (len x)) is finite (len D) + (len x) -element countable Element of K27(NAT)

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

(len D) + n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i . ((len D) + n) is set

x . n is set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i . n is set

D . n is set

i is set

Sgm i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

rng (Sgm i) is finite countable Element of K27(NAT)

x is set

dom (Sgm i) is finite countable set

(Sgm i) . x is set

n is set

(Sgm i) . n is set

dom (Sgm i) is finite countable Element of K27(NAT)

len (Sgm i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (len (Sgm i)) is finite len (Sgm i) -element countable Element of K27(NAT)

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

D is finite countable set

Sgm D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

len (Sgm D) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

card D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom (Sgm D) is finite countable Element of K27(NAT)

Seg (len (Sgm D)) is finite len (Sgm D) -element countable Element of K27(NAT)

card (Seg (len (Sgm D))) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

rng (Sgm D) is finite countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

D is finite countable set

Sgm D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

dom (Sgm D) is finite countable Element of K27(NAT)

card D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (card D) is finite card D -element countable Element of K27(NAT)

len (Sgm D) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is set

Sgm i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

len (Sgm i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

(Sgm i) . m9 is set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

(Sgm i) . n is set

i is set

Sgm i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

D is set

i \/ D is set

Sgm (i \/ D) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Sgm D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

(Sgm i) ^ (Sgm D) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg x is finite x -element countable Element of K27(NAT)

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg n is finite n -element countable Element of K27(NAT)

dom (Sgm i) is finite countable Element of K27(NAT)

i /\ D is set

the Element of i /\ D is Element of i /\ D

rng (Sgm i) is finite countable Element of K27(NAT)

a is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

len (Sgm (i \/ D)) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is finite countable set

t is finite countable set

n \/ t is finite countable set

card (n \/ t) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

card n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

card t is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(card n) + (card t) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

len (Sgm i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len (Sgm i)) + (card t) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

len (Sgm D) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len (Sgm i)) + (len (Sgm D)) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

g is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . g is set

(Sgm i) . g is set

g + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . (g + 1) is set

(Sgm i) . (g + 1) is set

rng (Sgm i) is finite countable Element of K27(NAT)

a is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (len (Sgm i)) is finite len (Sgm i) -element countable Element of K27(NAT)

Seg (len (Sgm (i \/ D))) is finite len (Sgm (i \/ D)) -element countable Element of K27(NAT)

dom (Sgm (i \/ D)) is finite countable Element of K27(NAT)

rng (Sgm (i \/ D)) is finite countable Element of K27(NAT)

f is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

x is set

(Sgm i) . x is set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

w is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

x is set

(Sgm (i \/ D)) . x is set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

s is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

w is set

(Sgm i) . w is set

s is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

w is set

(Sgm (i \/ D)) . w is set

s is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . 0 is set

(Sgm i) . 0 is set

dom (Sgm D) is finite countable Element of K27(NAT)

g is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len (Sgm i)) + g is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . ((len (Sgm i)) + g) is set

(Sgm D) . g is set

g + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

(len (Sgm i)) + (g + 1) is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . ((len (Sgm i)) + (g + 1)) is set

(Sgm D) . (g + 1) is set

dom (Sgm (i \/ D)) is finite countable Element of K27(NAT)

rng (Sgm (i \/ D)) is finite countable Element of K27(NAT)

f is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

rng (Sgm i) is finite countable Element of K27(NAT)

w is set

(Sgm i) . w is set

s is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . s is set

(len (Sgm i)) + 0 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

rng (Sgm D) is finite countable Element of K27(NAT)

w is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

x is set

(Sgm D) . x is set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

((len (Sgm i)) + g) + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

s is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

x is set

(Sgm (i \/ D)) . x is set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

((len (Sgm i)) + g) + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

s is set

(Sgm D) . s is set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len (Sgm i)) + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

s is set

(Sgm (i \/ D)) . s is set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm i) . x is set

(len (Sgm i)) + 0 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . ((len (Sgm i)) + 0) is set

(Sgm D) . 0 is set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

t is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

rng (Sgm D) is finite countable Element of K27(NAT)

dom (Sgm D) is finite countable Element of K27(NAT)

g is set

(Sgm D) . g is set

len (Sgm i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

a is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len (Sgm i)) + a is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (i \/ D)) . ((len (Sgm i)) + a) is set

len (Sgm D) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len (Sgm i)) + (len (Sgm D)) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

len (Sgm (i \/ D)) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

rng (Sgm i) is finite countable Element of K27(NAT)

dom (Sgm i) is finite countable Element of K27(NAT)

f is set

(Sgm i) . f is set

w is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (len (Sgm i)) is finite len (Sgm i) -element countable Element of K27(NAT)

(Sgm (i \/ D)) . w is set

Sgm {} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

{i} is non empty trivial finite V40() 1 -element countable set

Sgm {i} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

Seg i is finite i -element countable Element of K27(NAT)

len (Sgm {i}) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

card {i} is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

rng (Sgm {i}) is finite countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

{i,D} is non empty finite V40() countable set

Sgm {i,D} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*i,D*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like countable set

Seg D is finite D -element countable Element of K27(NAT)

Seg i is finite i -element countable Element of K27(NAT)

len (Sgm {i,D}) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

card {i,D} is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

dom (Sgm {i,D}) is finite countable Element of K27(NAT)

rng (Sgm {i,D}) is finite countable Element of K27(NAT)

(Sgm {i,D}) . 2 is set

(Sgm {i,D}) . 1 is set

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

Sgm (Seg i) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

len (Sgm (Seg i)) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

card (Seg i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + 0 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (i + 0) is finite i + 0 -element countable Element of K27(NAT)

Sgm (Seg (i + 0)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Seg i is finite i -element countable Element of K27(NAT)

(Sgm (Seg (i + 0))) | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

K28(NAT,NAT) is Relation-like non empty non trivial non finite set

K27(K28(NAT,NAT)) is non empty non trivial non finite set

Sgm (Seg i) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

card (Seg i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

len (Sgm (Seg i)) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom (Sgm (Seg i)) is finite countable Element of K27(NAT)

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

D + (i + 1) is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (D + (i + 1)) is non empty finite D + (i + 1) -element countable Element of K27(NAT)

Sgm (Seg (D + (i + 1))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

D + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (D + 1) is non empty finite D + 1 -element countable Element of K27(NAT)

Sgm (Seg (D + 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Seg D is finite D -element countable Element of K27(NAT)

(Sgm (Seg (D + 1))) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

K28(NAT,NAT) is Relation-like non empty non trivial non finite set

K27(K28(NAT,NAT)) is non empty non trivial non finite set

Sgm (Seg D) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

len (Sgm (Seg (D + 1))) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom (Sgm (Seg (D + 1))) is finite countable Element of K27(NAT)

m9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

dom m9 is finite countable Element of K27(NAT)

rng (Sgm (Seg (D + 1))) is finite countable Element of K27(NAT)

(Sgm (Seg (D + 1))) . (D + 1) is set

n is set

(Sgm (Seg (D + 1))) . n is set

{(D + 1)} is non empty trivial finite V40() 1 -element countable set

(Seg (D + 1)) \ {(D + 1)} is finite countable Element of K27(NAT)

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

rng m9 is finite countable Element of K27(NAT)

{((Sgm (Seg (D + 1))) . (D + 1))} is non empty trivial finite 1 -element countable set

(rng (Sgm (Seg (D + 1)))) \ {((Sgm (Seg (D + 1))) . (D + 1))} is finite countable Element of K27(NAT)

n is set

{(D + 1)} is non empty trivial finite V40() 1 -element countable set

n is set

m9 . n is set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (Seg (D + 1))) . n is set

m9 . n is set

n is set

n is set

(Sgm (Seg (D + 1))) . n is set

{(D + 1)} is non empty trivial finite V40() 1 -element countable set

(Seg (D + 1)) \ {(D + 1)} is finite countable Element of K27(NAT)

m9 . n is set

len m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

m9 . n is set

t is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

m9 . n is set

(Sgm (Seg (D + 1))) . n is set

(Sgm (Seg (D + 1))) . n is set

(D + 1) + i is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg ((D + 1) + i) is non empty finite (D + 1) + i -element countable Element of K27(NAT)

Sgm (Seg ((D + 1) + i)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

(Sgm (Seg (D + (i + 1)))) | (Seg (D + 1)) is Relation-like NAT -defined Seg (D + 1) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

(Seg (D + 1)) /\ (Seg D) is finite countable Element of K27(NAT)

(Sgm (Seg (D + (i + 1)))) | ((Seg (D + 1)) /\ (Seg D)) is Relation-like NAT -defined (Seg (D + 1)) /\ (Seg D) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

(Sgm (Seg (D + (i + 1)))) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

x + (D + 1) is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable set

Seg (x + (D + 1)) is non empty finite x + (D + 1) -element countable Element of K27(NAT)

Sgm (Seg (x + (D + 1))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Seg x is finite x -element countable Element of K27(NAT)

(Sgm (Seg (x + (D + 1)))) | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

Sgm (Seg x) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D + 0 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg (D + 0) is finite D + 0 -element countable Element of K27(NAT)

Sgm (Seg (D + 0)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Seg D is finite D -element countable Element of K27(NAT)

(Sgm (Seg (D + 0))) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

Sgm (Seg D) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D + i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg (D + i) is finite D + i -element countable Element of K27(NAT)

Sgm (Seg (D + i)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Seg D is finite D -element countable Element of K27(NAT)

(Sgm (Seg (D + i))) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

Sgm (Seg D) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg (i + D) is finite i + D -element countable Element of K27(NAT)

Sgm (Seg (i + D)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Seg i is finite i -element countable Element of K27(NAT)

(Sgm (Seg (i + D))) | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

Sgm (Seg i) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

Sgm (Seg i) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

idseq i is Relation-like NAT -defined Function-like finite i -element FinSequence-like FinSubsequence-like countable set

id (Seg i) is Relation-like Seg i -defined Seg i -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg i),(Seg i)))

K28((Seg i),(Seg i)) is Relation-like finite countable set

K27(K28((Seg i),(Seg i))) is non empty finite V40() countable set

i + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

idseq (i + 1) is Relation-like NAT -defined Function-like finite i + 1 -element FinSequence-like FinSubsequence-like countable set

Seg (i + 1) is non empty finite i + 1 -element countable Element of K27(NAT)

id (Seg (i + 1)) is Relation-like Seg (i + 1) -defined Seg (i + 1) -valued Function-like one-to-one non empty total quasi_total finite countable Element of K27(K28((Seg (i + 1)),(Seg (i + 1))))

K28((Seg (i + 1)),(Seg (i + 1))) is Relation-like non empty finite countable set

K27(K28((Seg (i + 1)),(Seg (i + 1)))) is non empty finite V40() countable set

len (idseq (i + 1)) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

Sgm (Seg (i + 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

len (Sgm (Seg (i + 1))) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom (Sgm (Seg (i + 1))) is finite countable Element of K27(NAT)

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

{(i + 1)} is non empty trivial finite V40() 1 -element countable set

(Seg i) \/ {(i + 1)} is non empty finite countable set

(idseq (i + 1)) . D is set

(Sgm (Seg (i + 1))) | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

(Sgm (Seg i)) . D is set

(Sgm (Seg (i + 1))) . D is set

rng (Sgm (Seg (i + 1))) is finite countable Element of K27(NAT)

(Sgm (Seg (i + 1))) . D is set

{D} is non empty trivial finite V40() 1 -element countable set

(Seg (i + 1)) \ {(i + 1)} is finite countable Element of K27(NAT)

(Sgm (Seg (i + 1))) | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like countable Element of K27(K28(NAT,NAT))

m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(Sgm (Seg (i + 1))) . m9 is set

(Sgm (Seg i)) . m9 is set

(idseq (i + 1)) . D is set

(Sgm (Seg (i + 1))) . D is set

(idseq (i + 1)) . D is set

(Sgm (Seg (i + 1))) . D is set

(idseq (i + 1)) . D is set

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

Sgm (Seg i) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

idseq i is Relation-like NAT -defined Function-like finite i -element FinSequence-like FinSubsequence-like countable set

id (Seg i) is Relation-like Seg i -defined Seg i -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg i),(Seg i)))

K28((Seg i),(Seg i)) is Relation-like finite countable set

K27(K28((Seg i),(Seg i))) is non empty finite V40() countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

Sgm (Seg D) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

idseq D is Relation-like NAT -defined Function-like finite D -element FinSequence-like FinSubsequence-like countable set

id (Seg D) is Relation-like Seg D -defined Seg D -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg D),(Seg D)))

K28((Seg D),(Seg D)) is Relation-like finite countable set

K27(K28((Seg D),(Seg D))) is non empty finite V40() countable set

D + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg (D + 1) is non empty finite D + 1 -element countable Element of K27(NAT)

Sgm (Seg (D + 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

idseq (D + 1) is Relation-like NAT -defined Function-like finite D + 1 -element FinSequence-like FinSubsequence-like countable set

id (Seg (D + 1)) is Relation-like Seg (D + 1) -defined Seg (D + 1) -valued Function-like one-to-one non empty total quasi_total finite countable Element of K27(K28((Seg (D + 1)),(Seg (D + 1))))

K28((Seg (D + 1)),(Seg (D + 1))) is Relation-like non empty finite countable set

K27(K28((Seg (D + 1)),(Seg (D + 1)))) is non empty finite V40() countable set

Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of K27(NAT)

Sgm (Seg 0) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

idseq 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() V33() Function-yielding V35() finite finite-yielding V40() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set

id (Seg 0) is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -valued Function-like one-to-one constant functional empty total V15() V16() V17() V19() V20() V21() ext-real non positive non negative V25() V26() quasi_total V33() Function-yielding V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of K27(K28((Seg 0),(Seg 0)))

K28((Seg 0),(Seg 0)) is Relation-like finite countable set

K27(K28((Seg 0),(Seg 0))) is non empty finite V40() countable set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

i | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like finite FinSubsequence-like countable set

Seg (len i) is finite len i -element countable Element of K27(NAT)

dom i is finite countable Element of K27(NAT)

(dom i) /\ (Seg D) is finite countable Element of K27(NAT)

x is set

i . x is set

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg i is finite i -element countable Element of K27(NAT)

idseq i is Relation-like NAT -defined Function-like finite i -element FinSequence-like FinSubsequence-like countable set

id (Seg i) is Relation-like Seg i -defined Seg i -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg i),(Seg i)))

K28((Seg i),(Seg i)) is Relation-like finite countable set

K27(K28((Seg i),(Seg i))) is non empty finite V40() countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i + D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

idseq (i + D) is Relation-like NAT -defined Function-like finite i + D -element FinSequence-like FinSubsequence-like countable set

Seg (i + D) is finite i + D -element countable Element of K27(NAT)

id (Seg (i + D)) is Relation-like Seg (i + D) -defined Seg (i + D) -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg (i + D)),(Seg (i + D))))

K28((Seg (i + D)),(Seg (i + D))) is Relation-like finite countable set

K27(K28((Seg (i + D)),(Seg (i + D)))) is non empty finite V40() countable set

(idseq (i + D)) | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined Function-like finite FinSubsequence-like countable set

Sgm (Seg i) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Sgm (Seg (i + D)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

idseq i is Relation-like NAT -defined Function-like finite i -element FinSequence-like FinSubsequence-like countable set

Seg i is finite i -element countable Element of K27(NAT)

id (Seg i) is Relation-like Seg i -defined Seg i -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg i),(Seg i)))

K28((Seg i),(Seg i)) is Relation-like finite countable set

K27(K28((Seg i),(Seg i))) is non empty finite V40() countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

(idseq i) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like finite FinSubsequence-like countable set

idseq D is Relation-like NAT -defined Function-like finite D -element FinSequence-like FinSubsequence-like countable set

id (Seg D) is Relation-like Seg D -defined Seg D -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg D),(Seg D)))

K28((Seg D),(Seg D)) is Relation-like finite countable set

K27(K28((Seg D),(Seg D))) is non empty finite V40() countable set

len (idseq D) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

len (idseq i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

D + x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

idseq i is Relation-like NAT -defined Function-like finite i -element FinSequence-like FinSubsequence-like countable set

Seg i is finite i -element countable Element of K27(NAT)

id (Seg i) is Relation-like Seg i -defined Seg i -valued Function-like one-to-one total quasi_total finite countable Element of K27(K28((Seg i),(Seg i)))

K28((Seg i),(Seg i)) is Relation-like finite countable set

K27(K28((Seg i),(Seg i))) is non empty finite V40() countable set

D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg D is finite D -element countable Element of K27(NAT)

(idseq i) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like finite FinSubsequence-like countable set

len (idseq i) is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg x is finite x -element countable Element of K27(NAT)

i | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined Function-like finite FinSubsequence-like countable set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

x + n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom D is finite countable Element of K27(NAT)

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

Seg x is finite x -element countable Element of K27(NAT)

i | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined Function-like finite FinSubsequence-like countable set

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

x + n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

len D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

x is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable set

x + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

Seg x is finite x -element countable Element of K27(NAT)

i | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined Function-like finite FinSubsequence-like countable set

i . (x + 1) is set

<*(i . (x + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable set

D ^ <*(i . (x + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like countable set

dom D is finite countable Element of K27(NAT)

n is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i . n is set

D . n is set

m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

dom <*(i . (x + 1))*> is non empty trivial finite 1 -element countable Element of K27(NAT)

len D is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

(len D) + m9 is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT

i . ((len D) + m9) is set

<*(i . (x + 1))*> . m9 is set

(len D) + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

len <*(i . (x + 1))*> is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

(len D) + (len <*(i . (x + 1))*>) is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom i is finite countable Element of K27(NAT)

D is set

i | D is Relation-like NAT -defined D -defined NAT -defined Function-like finite FinSubsequence-like countable set

D /\ (dom i) is finite countable Element of K27(NAT)

dom (i | D) is finite countable Element of K27(D)