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)