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

{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real non positive non negative V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

the Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real non positive non negative V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real non positive non negative V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered 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

card {} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real non positive non negative V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

Seg 1 is non empty V19() finite 1 -element Element of K37(NAT)

{ b

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

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

{ b

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

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

{ b

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

{ b

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

{ b

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

0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real non positive non negative V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

dom {} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real non positive non negative V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

rng {} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V19() ext-real non positive non negative V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_non-empty_elements set

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like 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

D is Relation-like Function-like set

rng D is set

D " is Relation-like Function-like set

M is set

(D ") . M is set

(D,M) is set

dom D is set

k is set

D . k is set

D is Relation-like Function-like set

M is set

D . M is set

(D,(D . M)) is set

dom D is set

D is Relation-like Function-like 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

<*M,k*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set

<*M*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,M] is set

{1,M} is non empty finite set

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

{[1,M]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*k*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,k] is set

{1,k} is non empty finite set

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

{[1,k]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*M*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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

<*M,k,f*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set

<*M*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,M] is set

{1,M} is non empty finite set

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

{[1,M]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*k*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,k] is set

{1,k} is non empty finite set

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

{[1,k]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*M*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set

<*f*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,f] is set

{1,f} is non empty finite set

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

{[1,f]} is Relation-like Function-like constant non empty V19() finite 1 -element set

(<*M*> ^ <*k*>) ^ <*f*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like 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

k is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M

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

<*M*> is Relation-like NAT -defined D -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of D

[1,M] is set

{1,M} is non empty finite set

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

{[1,M]} is Relation-like Function-like constant non empty V19() finite 1 -element 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

(D,M,k) is Relation-like NAT -defined D -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of D

<*M*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,M] is set

{1,M} is non empty finite set

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

{[1,M]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*k*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,k] is set

{1,k} is non empty finite set

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

{[1,k]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*M*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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

(D,M,k,f) is Relation-like NAT -defined D -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of D

<*M*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,M] is set

{1,M} is non empty finite set

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

{[1,M]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*k*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,k] is set

{1,k} is non empty finite set

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

{[1,k]} is Relation-like Function-like constant non empty V19() finite 1 -element set

<*M*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set

<*f*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,f] is set

{1,f} is non empty finite set

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

{[1,f]} is Relation-like Function-like constant non empty V19() finite 1 -element set

(<*M*> ^ <*k*>) ^ <*f*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like 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

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

M is set

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

D " {M} is finite set

Sgm (D " {M}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

rng (Sgm (D " {M})) is finite set

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

rng (Sgm (D " {M})) is finite set

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

dom D is finite Element of K37(NAT)

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

D . (D,M) is set

dom D is finite Element of K37(NAT)

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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)

{ b

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

rng D is finite set

dom D is finite Element of K37(NAT)

D . (D,M) is set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

k is set

D . k is set

D . (D,M) is set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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

D - {M} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence 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

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

M is set

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

D - {M} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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

{ b

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)

{ b

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)

{ b

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

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

rng D is finite set

M is set

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

D - {M} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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)

{ b

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Seg x is finite x -element Element of K37(NAT)

{ b

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

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

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Seg y is finite y -element Element of K37(NAT)

{ b

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

(D,M) - 1 is ext-real V31() V32() V33() set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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)

{ b

D | (Seg k) is Relation-like NAT -defined Seg k -defined NAT -defined Function-like finite FinSubsequence-like 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)

{ b

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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

D | (Seg k) is Relation-like NAT -defined Seg k -defined NAT -defined Function-like finite FinSubsequence-like 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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

(D,M) - 1 is ext-real V31() V32() V33() set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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)

{ b

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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

D | (Seg k) is Relation-like NAT -defined Seg k -defined NAT -defined Function-like finite FinSubsequence-like 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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (D,M) is finite set

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

k is set

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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

M is set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(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

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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)

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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)

{ b

Seg (len f) is finite len f -element Element of K37(NAT)

{ b

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

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

(len D) - (D,M) is ext-real V31() V32() V33() set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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)

{ b

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

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

rng D is finite set

dom D is finite Element of K37(NAT)

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(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

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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

{ b

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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (D,M) is finite set

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

k is set

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (D,M) is finite set

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

k is set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{ b

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)

{ b

dom D is finite Element of K37(NAT)

D . (y + (D,M)) is set

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

rng D is finite set

M is set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

<*M*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

[1,M] is set

{1,M} is non empty finite set

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

{[1,M]} is Relation-like Function-like constant non empty V19() finite 1 -element set

(D,M) ^ <*M*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

((D,M) ^ <*M*>) ^ (D,M) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like 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}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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