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

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

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

INT 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

D is set
len i is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of 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

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

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

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

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

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

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

the Element of rng i is Element of rng i
i is set
D is set

i is set
D is set
x is set

i is set

D is set
x is 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
x is set
n is 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

x is set
n is set
m9 is 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

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

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

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

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

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

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

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

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

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

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

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

D is set
i \/ D is set

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

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

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

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

len () 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 () 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

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

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)

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

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)

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)

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

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)

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

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)

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)

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)

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)

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

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

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

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)) . 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)

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

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

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)

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

K28((),()) is Relation-like finite countable set
K27(K28((),())) is non empty finite V40() 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

(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

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

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

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

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

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 () is V15() V16() V17() V21() ext-real non negative V25() V26() V33() finite cardinal countable Element of NAT
len () 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

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

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

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

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

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

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

len 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
x + 1 is non empty V15() V16() V17() V21() ext-real positive non negative V25() V26() V33() finite cardinal countable Element of NAT

i . (x + 1) is set

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

D is set

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