:: FINSEQ_4 semantic presentation

REAL is set
NAT is V6() V7() V8() non empty V19() non finite cardinal limit_cardinal Element of K37(REAL)
K37(REAL) is non empty set
NAT is V6() V7() V8() non empty V19() non finite cardinal limit_cardinal set
K37(NAT) is non empty V19() non finite set
K37(NAT) is non empty V19() non finite set

1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
2 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
3 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT

Seg 1 is non empty V19() finite 1 -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty V19() finite V38() 1 -element set
Seg 2 is non empty finite 2 -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V38() set
Seg 3 is non empty finite 3 -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
{1,2,3} is non empty finite set
4 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg 4 is non empty finite 4 -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= 4 ) } is set
{1,2,3,4} is non empty finite set
5 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg 5 is non empty finite 5 -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= 5 ) } is set
{1,2,3,4,5} is non empty finite set

dom D is set
M is set
Im (D,M) is set
{M} is non empty V19() finite 1 -element set
D .: {M} is finite set
D " (Im (D,M)) is set

dom D is set
M is set
D . M is set
{(D . M)} is non empty V19() finite 1 -element set
D " {(D . M)} is set
{M} is non empty V19() finite 1 -element set
Im (D,M) is set
D .: {M} is finite set
D " (Im (D,M)) is set
Im (D,M) is set
D .: {M} is finite set
D " (Im (D,M)) is set

dom D is set
M is set
D . M is set
k is set
D . k is set
{(D . M)} is non empty V19() finite 1 -element set
D " {(D . M)} is set
{M} is non empty V19() finite 1 -element set
{(D . M)} is non empty V19() finite 1 -element set
D " {(D . M)} is set
{M} is non empty V19() finite 1 -element set
k is set
D . k is set

dom D is set
M is set
D . M is set
k is set
D . k is set
M is set
D . M is set
k is set
D . k is set

rng D is set
M is set
Coim (D,M) is set
{M} is non empty V19() finite 1 -element set
D " {M} is set
card (Coim (D,M)) is V6() V7() V8() cardinal set
(rng D) /\ {M} is finite set
k is set

M is set
{M} is non empty V19() finite 1 -element set
D " {M} is set
rng D is set
dom D is set
k is set
D . k is set
{k} is non empty V19() finite 1 -element set
Coim (D,M) is set
card (Coim (D,M)) is V6() V7() V8() cardinal set
f is set
{f} is non empty V19() finite 1 -element set
Coim (D,M) is set
card (Coim (D,M)) is V6() V7() V8() cardinal set
k is set
{k} is non empty V19() finite 1 -element set

dom D is set
M is set
Coim (D,M) is set
{M} is non empty V19() finite 1 -element set
D " {M} is set
card (Coim (D,M)) is V6() V7() V8() cardinal set
rng D is set
k is set
D . k is set
f is set
D . f is set
{f,k} is non empty finite set
card {f,k} is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
k is set
D . k is set
{k} is non empty V19() finite 1 -element set
{M} is non empty V19() finite 1 -element set
D " {M} is set
f is set
f is set
D . f is set
Coim (D,M) is set
card (Coim (D,M)) is V6() V7() V8() cardinal set

rng D is set
M is set
dom D is set
k is set
D . k is set
f is set
D . f is set
M is set
dom D is set
D . M is set
k is set
D . k is set
{(D . M)} is non empty V19() finite 1 -element set
D " {(D . M)} is set
f is set
{f} is non empty V19() finite 1 -element set

dom D is set
M is set
D . M is set
{M} is non empty V19() finite 1 -element set
{(D . M)} is non empty V19() finite 1 -element set
D " {(D . M)} is set
{(D . M)} is non empty V19() finite 1 -element set
D " {(D . M)} is set
k is set
{k} is non empty V19() finite 1 -element set

M is set
dom D is set
rng D is set
k is set
D . k is set
k is set
D . k is set
f is set
D . f is set
x is set
D . x is set

M is set
(D,M) is set
Im (D,(D,M)) is set
{(D,M)} is non empty V19() finite 1 -element set
D .: {(D,M)} is finite set
{M} is non empty V19() finite 1 -element set
dom D is set
D . (D,M) is set
{(D . (D,M))} is non empty V19() finite 1 -element set

M is set
{M} is non empty V19() finite 1 -element set
D " {M} is set
(D,M) is set
{(D,M)} is non empty V19() finite 1 -element set
k is set
{k} is non empty V19() finite 1 -element set
D . k is set
dom D is set

rng D is set

M is set
(D ") . M is set
(D,M) is set
dom D is set
k is set
D . k is set

M is set
D . M is set
(D,(D . M)) is set
dom D is set

M is set
(D,M) is set
k is set
dom D is set
D . k is set
D . (D,M) is set
D is non empty set
M is Element of D
k is Element of D

[1,M] is set
{1,M} is non empty finite set
{{1,M},{1}} is non empty finite V38() set

[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V38() set

1 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D is non empty set
M is Element of D
k is Element of D
f is Element of D

[1,M] is set
{1,M} is non empty finite set
{{1,M},{1}} is non empty finite V38() set

[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V38() set

[1,f] is set
{1,f} is non empty finite set
{{1,f},{1}} is non empty finite V38() set

(1 + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M is set

len k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k /. D is Element of M
k . D is set
dom k is finite Element of K37(NAT)
D is non empty set
M is Element of D

[1,M] is set
{1,M} is non empty finite set
{{1,M},{1}} is non empty finite V38() set

<*M*> /. 1 is Element of D
dom <*M*> is non empty V19() finite 1 -element Element of K37(NAT)
<*M*> . 1 is set
D is non empty set
M is Element of D
k is Element of D

[1,M] is set
{1,M} is non empty finite set
{{1,M},{1}} is non empty finite V38() set

[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V38() set

(D,M,k) /. 1 is Element of D
(D,M,k) /. 2 is Element of D
(D,M,k) . 2 is set
dom (D,M,k) is non empty finite 2 -element Element of K37(NAT)
(D,M,k) . 1 is set
D is non empty set
M is Element of D
k is Element of D
f is Element of D

[1,M] is set
{1,M} is non empty finite set
{{1,M},{1}} is non empty finite V38() set

[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V38() set

[1,f] is set
{1,f} is non empty finite set
{{1,f},{1}} is non empty finite V38() set

(D,M,k,f) /. 1 is Element of D
(D,M,k,f) /. 2 is Element of D
(D,M,k,f) /. 3 is Element of D
(D,M,k,f) . 2 is set
(D,M,k,f) . 3 is set
dom (D,M,k,f) is non empty finite 3 -element Element of K37(NAT)
(D,M,k,f) . 1 is set

M is set
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
dom (Sgm (D " {M})) is finite Element of K37(NAT)
dom (Sgm (D " {M})) is finite Element of K37(NAT)
rng (Sgm (D " {M})) is finite set
dom (Sgm (D " {M})) is finite Element of K37(NAT)

rng D is finite set
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
D . (D,M) is set
dom D is finite Element of K37(NAT)
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len D) is finite len D -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len D ) } is set
rng (Sgm (D " {M})) is finite set
dom (Sgm (D " {M})) is finite Element of K37(NAT)

rng D is finite set
dom D is finite Element of K37(NAT)
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len D) is finite len D -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len D ) } is set
rng (Sgm (D " {M})) is finite set
dom (Sgm (D " {M})) is finite Element of K37(NAT)

rng D is finite set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
dom D is finite Element of K37(NAT)

rng D is finite set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
(len D) - (D,M) is ext-real V31() V32() V33() set

rng D is finite set
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
D . (D,M) is set
dom D is finite Element of K37(NAT)

dom D is finite Element of K37(NAT)
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
D . k is set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len D) is finite len D -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len D ) } is set
rng (Sgm (D " {M})) is finite set
dom (Sgm (D " {M})) is finite Element of K37(NAT)
x is set
(Sgm (D " {M})) . x is set
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
len (Sgm (D " {M})) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len (Sgm (D " {M}))) is finite len (Sgm (D " {M})) -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Sgm (D " {M})) ) } is set

M is set
(D,M) is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
rng D is finite set
dom D is finite Element of K37(NAT)
D . (D,M) is set

dom D is finite Element of K37(NAT)
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
D . k is set
(D,M) is set

rng D is finite set
dom D is finite Element of K37(NAT)
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
k is set
D . k is set
D . (D,M) is set

rng D is finite set
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
{(D,M)} is non empty V19() finite V38() 1 -element set
(D,M) is set
k is set
dom D is finite Element of K37(NAT)
D . k is set
D . (D,M) is set

rng D is finite set
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
{(D,M)} is non empty V19() finite V38() 1 -element set
k is set
k is set
dom D is finite Element of K37(NAT)
D . k is set
D . (D,M) is set

len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - 1 is ext-real V31() V32() V33() set
M is set
{M} is non empty V19() finite 1 -element set

len (D - {M}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D " {M} is finite set
card (D " {M}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - (card (D " {M})) is ext-real V31() V32() V33() set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT

(Sgm (D " {M})) . 1 is set
{(D,M)} is non empty V19() finite V38() 1 -element set
D " {M} is finite set
Coim (D,M) is set
- 1 is ext-real non positive V31() V32() V33() set
(len D) + (- 1) is ext-real V31() V32() V33() set
card (D " {M}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - (card (D " {M})) is ext-real V31() V32() V33() set
- (card (D " {M})) is ext-real non positive V31() V32() V33() set
(len D) + (- (card (D " {M}))) is ext-real V31() V32() V33() set

M is set
{M} is non empty V19() finite 1 -element set

dom (D - {M}) is finite Element of K37(NAT)
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(D - {M}) . f is set
D . f is set
f + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D . (f + 1) is set
dom D is finite Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( b1 in dom D & b1 <= f & D . b1 in {M} ) } is set
y is set
y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . y9 is set
f - 0 is ext-real non negative V31() V32() V33() set
(D - {M}) . (f - 0) is set
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( b1 in dom D & b1 <= f + 1 & D . b1 in {M} ) } is set
rng D is finite set
{(D,M)} is non empty V19() finite V38() 1 -element set
y9 is set
a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . a is set
y9 is set
D . (D,M) is set
len (D - {M}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len (D - {M})) is finite len (D - {M}) -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (D - {M}) ) } is set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - 1 is ext-real V31() V32() V33() set
Seg (len D) is finite len D -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len D ) } is set
y9 is finite set
card y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(f + 1) - (card y9) is ext-real V31() V32() V33() set
(D - {M}) . ((f + 1) - (card y9)) is set
(f + 1) - 1 is ext-real V31() V32() V33() set
(D - {M}) . ((f + 1) - 1) is set

rng D is finite set
M is set
{M} is non empty V19() finite 1 -element set

dom (D - {M}) is finite Element of K37(NAT)
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(D - {M}) . f is set
D . f is set
f + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D . (f + 1) is set
len (D - {M}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len (D - {M})) is finite len (D - {M}) -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (D - {M}) ) } is set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - 1 is ext-real V31() V32() V33() set
Seg (len D) is finite len D -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len D ) } is set
dom D is finite Element of K37(NAT)
f + 0 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
f + 0 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M is set

rng D is finite set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg k is finite k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set

Seg x is finite x -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= x ) } is set

y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set

Seg y is finite y -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= y ) } is set

rng D is finite set
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set

k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg k is finite k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg f is finite f -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

rng D is finite set
M is set

len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg k is finite k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

k + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT

rng D is finite set
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set

dom (D,M) is finite Element of K37(NAT)
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg k is finite k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT

rng D is finite set
M is set

dom (D,M) is finite Element of K37(NAT)
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
D . k is set
(D,M) . k is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg f is finite f -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

rng D is finite set
M is set

rng (D,M) is finite set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg k is finite k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

dom (D | (Seg k)) is finite set
x is set
(D | (Seg k)) . x is set
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
dom D is finite Element of K37(NAT)
D . y is set

rng D is finite set
M is set

rng (D,M) is finite set
{M} is non empty V19() finite 1 -element set
k is set

rng D is finite set
M is set

rng (D,M) is finite set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg k is finite k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

rng D is finite set
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set

len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) - 1 is ext-real V31() V32() V33() set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) - 1 is ext-real V31() V32() V33() set

rng D is finite set
M is set

k is non empty set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg f is finite f -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

M is set

rng D is finite set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(len D) - (D,M) is ext-real V31() V32() V33() set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT

len f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom f is finite Element of K37(NAT)
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
f . x is set
x + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . (x + (D,M)) is set

len k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom k is finite Element of K37(NAT)

len f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom f is finite Element of K37(NAT)
Seg (len k) is finite len k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len k ) } is set
Seg (len f) is finite len f -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
k . x is set
x + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . (x + (D,M)) is set
f . x is set

rng D is finite set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(len D) - (D,M) is ext-real V31() V32() V33() set

dom (D,M) is finite Element of K37(NAT)
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg k is finite k -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT

rng D is finite set
dom D is finite Element of K37(NAT)
M is set

dom (D,M) is finite Element of K37(NAT)
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
k + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - (D,M) is ext-real V31() V32() V33() set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg f is finite f -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

rng D is finite set
M is set

rng (D,M) is finite set
k is set
dom (D,M) is finite Element of K37(NAT)
f is set
(D,M) . f is set
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
x + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . (x + (D,M)) is set
dom D is finite Element of K37(NAT)

rng D is finite set
M is set

rng (D,M) is finite set
dom (D,M) is finite Element of K37(NAT)
k is set
(D,M) . k is set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) . f is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
f + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . (f + (D,M)) is set
dom D is finite Element of K37(NAT)
0 + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
dom D is finite Element of K37(NAT)
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
D . k is set
k + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) - 1 is ext-real V31() V32() V33() set

len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom (D,M) is finite Element of K37(NAT)
(D,M) . k is set
rng (D,M) is finite set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(D,M) + f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) + 0 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
0 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
f + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - (D,M) is ext-real V31() V32() V33() set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom (D,M) is finite Element of K37(NAT)
(D,M) . f is set

rng D is finite set
M is set

rng (D,M) is finite set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(len D) - (D,M) is ext-real V31() V32() V33() set
dom (D,M) is finite Element of K37(NAT)
k is set
(D,M) . k is set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
f + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len (D,M)) is finite len (D,M) -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (D,M) ) } is set
Seg (len D) is finite len D -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len D ) } is set
dom D is finite Element of K37(NAT)
D . (D,M) is set
(D,M) . f is set
D . (f + (D,M)) is set
0 + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT

rng D is finite set
M is set

rng (D,M) is finite set
{M} is non empty V19() finite 1 -element set
k is set

rng D is finite set
M is set

rng (D,M) is finite set
{M} is non empty V19() finite 1 -element set
k is set

rng D is finite set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set

len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - (D,M) is ext-real V31() V32() V33() set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - (D,M) is ext-real V31() V32() V33() set

rng D is finite set
M is set

k is non empty set
rng (D,M) is finite set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(len D) - (D,M) is ext-real V31() V32() V33() set
f is set
dom (D,M) is finite Element of K37(NAT)
x is set
(D,M) . x is set
Seg (len (D,M)) is finite len (D,M) -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (D,M) ) } is set
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len D) is finite len D -element Element of K37(NAT)
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len D ) } is set
dom D is finite Element of K37(NAT)
D . (y + (D,M)) is set

rng D is finite set
M is set

[1,M] is set
{1,M} is non empty finite set
{{1,M},{1}} is non empty finite V38() set

y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom (D,M) is finite Element of K37(NAT)
(D,M) . y is set
(D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{M} is non empty V19() finite 1 -element set
D " {M} is finite set

(Sgm (D " {M})) . 1 is set
(D,M) - 1 is ext-real V31() V32() V33() set
((D,M) - 1) + 1 is ext-real V31() V32() V33() set
(((D,M) - 1) + 1) + y is ext-real V31() V32() V33() set
D . ((((D,M) - 1) + 1) + y) is set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len (D,M)) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
((len (D,M)) + 1) + y is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D . (((len (D,M)) + 1) + y) is set
len <*M*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len (D,M)) + () is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
((len (D,M)) + ()) + y is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D . (((len (D,M)) + ()) + y) is set
len ((D,M) ^ <*M*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len ((D,M) ^ <*M*>)) + y is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D . ((len ((D,M) ^ <*M*>)) + y) is set
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom ((D,M) ^ <*M*>) is non empty finite Element of K37(NAT)
dom (D,M) is finite Element of K37(NAT)
((D,M) ^ <*M*>) . y is set
(D,M) . y is set
D . y is set
dom <*M*> is non empty V19() finite 1 -element Element of K37(NAT)
y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len (D,M)) + y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len (D,M)) + y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
((D,M) ^ <*M*>) . y is set
<*M*> . 1 is set
D . (((D,M) - 1) + 1) is set
D . y is set
dom (D,M) is finite Element of K37(NAT)
dom <*M*> is non empty V19() finite 1 -element Element of K37(NAT)
((D,M) ^ <*M*>) . y is set
D . y is set
((D,M) ^ <*M*>) . y is set
D . y is set
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - (D,M) is ext-real V31() V32() V33() set
((len D) - (D,M)) + (D,M) is ext-real V31() V32() V33() set
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(((D,M) - 1) + 1) + (len (D,M)) is ext-real