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)
{ 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
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)
{ 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)
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)
{ 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)
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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)
{ 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
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 V31() V32() V33() set
((len (D,M)) + 1) + (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)) + (len <*M*>)) + (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) ^ <*M*>)) + (len (D,M)) is V6() V7() V8() V12() non empty ext-real positive 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
<*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
<*M*> ^ (D,M) is Relation-like NAT -defined Function-like non empty 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
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
(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) ^ <*M*>) ^ (D,M) is Relation-like NAT -defined Function-like non empty finite FinSequence-like 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
{M} is non empty V19() finite 1 -element set
D - {M} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) ^ (D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(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
len D 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) - 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
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
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
dom (D,M) is finite Element of K37(NAT)
dom (D - {M}) is finite Element of K37(NAT)
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
y + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(D,M) . y is set
D . y is set
(D - {M}) . y is set
y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y9 + 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) . y9 is set
y9 + (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . (y9 + (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
(D,M) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(y9 + (D,M)) - 1 is ext-real V31() V32() V33() set
(len D) - (D,M) is ext-real V31() V32() V33() set
1 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(D - {M}) . (y9 + y) is set
(y9 + y) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D . ((y9 + y) + 1) is set
(len (D,M)) + y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D - {M}) . ((len (D,M)) + y9) is set
(len (D,M)) + (len (D,M)) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
((D,M) - 1) + (len (D,M)) is ext-real V31() V32() V33() set
((D,M) - 1) + ((len D) - (D,M)) is ext-real V31() V32() V33() set
Seg ((len (D,M)) + (len (D,M))) is finite (len (D,M)) + (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)) + (len (D,M)) ) } is set
y 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
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 . y is set
{(D,M),y} is non empty finite V38() set
y9 is set
D . (D,M) is set
card {(D,M),y} is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
card (D " {M}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
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
(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
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
len (D,M) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len (D,M)) + (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,M) - 1) + (len (D,M)) is ext-real V31() V32() V33() set
(len D) - (D,M) is ext-real V31() V32() V33() set
((D,M) - 1) + ((len D) - (D,M)) is ext-real V31() V32() V33() set
- 1 is ext-real non positive V31() V32() V33() set
(len D) + (- 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
{M} is non empty V19() finite 1 -element set
D - {M} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) ^ (D,M) is Relation-like NAT -defined Function-like finite FinSequence-like 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
{M} is non empty V19() finite 1 -element set
D - {M} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(D,M) ^ (D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is set
dom D is finite set
D . f is set
x is set
D . x is 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
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 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
y9 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
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
y9 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
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
y 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
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
y 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 Element of NAT
len D 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
(len D) - 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
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
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
dom (D - {M}) is finite Element of K37(NAT)
(D - {M}) . y is set
D . y is set
a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
a + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
CE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D - {M}) . CE1a is set
D . y9 is set
(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
y 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 Element of NAT
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y9 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - 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
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
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
dom (D - {M}) is finite Element of K37(NAT)
D . y9 is set
(D - {M}) . y9 is set
y + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D . y is set
(D - {M}) . y is set
y 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
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
y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
a + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
CE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
CE1a + 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
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
p229 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
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
dom (D - {M}) is finite Element of K37(NAT)
D . y9 is set
(D - {M}) . p229 is set
fCE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D . y is set
(D - {M}) . fCE1a is set
y 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
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
y 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
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
y9 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
y9 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len D) - 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
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
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
dom (D - {M}) is finite Element of K37(NAT)
(D - {M}) . y9 is set
D . y9 is set
a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
a + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
CE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(D - {M}) . CE1a is set
D . y is set
(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
y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y 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
(D,M) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (D,M) is finite 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) ^ <*M*>) ^ (D,M) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
rng ((D,M) ^ <*M*>) is non empty finite set
D is set
M is set
k is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite 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
f ^ <*M*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
rng x is non empty finite set
rng <*M*> is non empty V19() finite 1 -element set
(rng f) \/ (rng <*M*>) is non empty finite set
{M} is non empty V19() finite 1 -element set
k \/ {M} is non empty set
y is set
dom x is non empty finite set
x . y is set
y9 is set
x . y9 is set
dom x is non empty finite Element of K37(NAT)
a 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)
dom <*M*> is non empty V19() finite 1 -element Element of K37(NAT)
CE1a 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
fCE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len f) + fCE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
<*M*> . fCE1a is set
x . a is set
f . a is set
fCE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len f) + fCE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
<*M*> . fCE1a is set
x . CE1a is set
f . CE1a is set
fCE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len f) + fCE1a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
p229 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len f) + p229 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng x is finite set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng x is finite set
y is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
rng y is non empty finite set
M is set
k is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
{M} is non empty V19() finite 1 -element set
k \/ {M} is non empty 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)
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M 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
len k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
rng k is finite set
dom k is finite Element of K37(NAT)
Seg (M + 1) is non empty finite M + 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 <= M + 1 ) } is set
f is set
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
{(M + 1)} is non empty V19() finite V38() 1 -element set
(Seg (M + 1)) \ {(M + 1)} is finite Element of K37(NAT)
Seg M is finite 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 <= M ) } is set
k - {(M + 1)} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (k - {(M + 1)}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(M + 1) - 1 is ext-real V31() V32() V33() set
dom (k - {(M + 1)}) is finite Element of K37(NAT)
rng (k - {(M + 1)}) is finite set
(rng k) \ {(M + 1)} is finite Element of K37((rng k))
K37((rng k)) is non empty finite V38() set
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg M is finite 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 <= M ) } is set
y is set
{(M + 1)} is non empty V19() finite V38() 1 -element set
(Seg (M + 1)) \ {(M + 1)} is finite Element of K37(NAT)
k . (M + 1) is set
k | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined Function-like finite FinSubsequence-like set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom y is finite Element of K37(NAT)
len y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
rng y is finite set
y9 is set
y . y9 is set
k . y9 is set
a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M 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
len k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
rng k is finite set
dom k is finite Element of K37(NAT)
M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
rng M is finite set
dom M is finite Element of K37(NAT)
M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
rng M is finite set
dom 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)
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M + 1 is V6() V7() V8() V12() non empty ext-real positive 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
rng f is finite set
dom f is finite Element of K37(NAT)
{(M + 1)} is non empty V19() finite V38() 1 -element set
f - {(M + 1)} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg (M + 1) is non empty finite M + 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 <= M + 1 ) } is set
rng (f - {(M + 1)}) is finite set
(Seg (M + 1)) \ {(M + 1)} is finite Element of K37(NAT)
Seg M is finite 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 <= M ) } is set
card (rng (f - {(M + 1)})) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
card M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(f,(M + 1)) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
f " {(M + 1)} is finite set
Sgm (f " {(M + 1)}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (f " {(M + 1)})) . 1 is set
f . (f,(M + 1)) is set
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
f . y is set
{(f,(M + 1)),y} is non empty finite V38() set
card {(f,(M + 1)),y} is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
card (f " {(M + 1)}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
len (f - {(M + 1)}) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(M + 1) - (card (f " {(M + 1)})) is ext-real V31() V32() V33() set
2 + (len (f - {(M + 1)})) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(card (f " {(M + 1)})) + ((M + 1) - (card (f " {(M + 1)}))) is ext-real V31() V32() V33() set
(len (f - {(M + 1)})) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
((len (f - {(M + 1)})) + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
M - 1 is ext-real V31() V32() V33() set
dom (f - {(M + 1)}) is finite Element of K37(NAT)
Seg (len (f - {(M + 1)})) is finite len (f - {(M + 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 <= len (f - {(M + 1)}) ) } is set
card (dom (f - {(M + 1)})) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
card (len (f - {(M + 1)})) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M + 0 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(M + 1) - 1 is ext-real V31() V32() V33() set
(f,(M + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f,(M + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f,(M + 1)) ^ (f,(M + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
rng M is finite set
dom 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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng M is finite set
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M " is Relation-like Function-like set
dom (M ") is set
D * (M ") is Relation-like NAT -defined Function-like finite set
dom (D * (M ")) is finite set
dom D is finite Element of K37(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
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng k is finite set
rng (M ") is set
dom M is finite Element of K37(NAT)
Seg (len M) is finite len 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 M ) } is set
D is finite set
M is finite set
K38(D,M) is Relation-like finite set
K37(K38(D,M)) is non empty finite V38() set
card D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
card M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k is Relation-like D -defined M -valued Function-like quasi_total finite Element of K37(K38(D,M))
rng k is finite set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
dom f is finite Element of K37(NAT)
f .: (dom f) is finite set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng y is finite set
dom y is finite Element of K37(NAT)
len y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len y) is finite len 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 <= len y ) } is set
y .: (dom y) is finite set
x is finite set
card x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
card (Seg (len y)) 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
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
card (Seg (len f)) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom k is finite set
f * k is Relation-like NAT -defined M -valued Function-like finite set
rng (f * k) is finite set
y " is Relation-like Function-like set
dom (y ") is set
k * (y ") is Relation-like D -defined Function-like finite set
dom (k * (y ")) is finite set
f * (k * (y ")) is Relation-like NAT -defined Function-like finite set
dom (f * (k * (y "))) is finite set
y9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f * k) * (y ") is Relation-like NAT -defined Function-like finite set
rng y9 is finite set
rng (y ") is set
y9 * y is Relation-like NAT -defined Function-like finite set
((f * k) * (y ")) * y is Relation-like NAT -defined Function-like finite set
(y ") * y is Relation-like Function-like set
(f * k) * ((y ") * y) is Relation-like NAT -defined Function-like finite set
id (rng y) is Relation-like rng y -defined rng y -valued Function-like one-to-one total quasi_total onto bijective finite V48() V50() V51() V55() Element of K37(K38((rng y),(rng y)))
K38((rng y),(rng y)) is Relation-like finite set
K37(K38((rng y),(rng y))) is non empty finite V38() set
(f * k) * (id (rng y)) is Relation-like NAT -defined rng y -valued Function-like finite set
(id (rng y)) * k is Relation-like D -defined rng y -valued Function-like finite Element of K37(K38(D,(rng y)))
K38(D,(rng y)) is Relation-like finite set
K37(K38(D,(rng y))) is non empty finite V38() set
f * ((id (rng y)) * k) is Relation-like NAT -defined rng y -valued Function-like finite set
f " is Relation-like Function-like set
(f ") * (y9 * y) is Relation-like Function-like set
(f ") * f is Relation-like Function-like set
((f ") * f) * k is Relation-like M -valued Function-like set
id (rng f) is Relation-like rng f -defined rng f -valued Function-like one-to-one total quasi_total onto bijective finite V48() V50() V51() V55() Element of K37(K38((rng f),(rng f)))
K38((rng f),(rng f)) is Relation-like finite set
K37(K38((rng f),(rng f))) is non empty finite V38() set
k * (id (rng f)) is Relation-like rng f -defined M -valued Function-like finite Element of K37(K38((rng f),M))
K38((rng f),M) is Relation-like finite set
K37(K38((rng f),M)) is non empty finite V38() set
id (dom k) is Relation-like dom k -defined dom k -valued Function-like one-to-one total quasi_total onto bijective finite V48() V50() V51() V55() Element of K37(K38((dom k),(dom k)))
K38((dom k),(dom k)) is Relation-like finite set
K37(K38((dom k),(dom k))) is non empty finite V38() set
k * (id (dom k)) is Relation-like dom k -defined M -valued Function-like finite Element of K37(K38((dom k),M))
K38((dom k),M) is Relation-like finite set
K37(K38((dom k),M)) is non empty finite V38() set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng D is finite set
card (rng D) 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
dom D is finite Element of K37(NAT)
D .: (dom D) is finite 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
card (Seg (len D)) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom D is finite Element of K37(NAT)
K38((dom D),(rng D)) is Relation-like finite set
K37(K38((dom D),(rng D))) is non empty finite V38() 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
card (Seg (len D)) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k is finite set
card k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M is Relation-like dom D -defined rng D -valued Function-like quasi_total finite Element of K37(K38((dom D),(rng D)))
dom M is finite set
D is finite set
M is finite set
K38(D,M) is Relation-like finite set
K37(K38(D,M)) is non empty finite V38() set
card D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
card M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k is Relation-like D -defined M -valued Function-like quasi_total finite Element of K37(K38(D,M))
rng k is finite set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
dom f is finite Element of K37(NAT)
f .: (dom f) is finite set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng x is finite set
dom x is finite Element of K37(NAT)
len x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len x) is finite len 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 <= len x ) } is set
x .: (dom x) is finite set
card (dom f) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
card (Seg (len x)) 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
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
card (Seg (len f)) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
x " is Relation-like Function-like set
dom (x ") is set
k * (x ") is Relation-like D -defined Function-like finite set
dom (k * (x ")) is finite set
dom k is finite set
f * (k * (x ")) is Relation-like NAT -defined Function-like finite set
dom (f * (k * (x "))) is finite set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f * k is Relation-like NAT -defined M -valued Function-like finite set
(f * k) * (x ") is Relation-like NAT -defined Function-like finite set
rng y is finite set
rng (x ") is set
dom y is finite Element of K37(NAT)
y * x is Relation-like NAT -defined Function-like finite set
rng (y * x) is finite set
((f * k) * (x ")) * x is Relation-like NAT -defined Function-like finite set
(x ") * x is Relation-like Function-like set
(f * k) * ((x ") * x) is Relation-like NAT -defined Function-like finite set
id (rng x) is Relation-like rng x -defined rng x -valued Function-like one-to-one total quasi_total onto bijective finite V48() V50() V51() V55() Element of K37(K38((rng x),(rng x)))
K38((rng x),(rng x)) is Relation-like finite set
K37(K38((rng x),(rng x))) is non empty finite V38() set
(f * k) * (id (rng x)) is Relation-like NAT -defined rng x -valued Function-like finite set
(id (rng x)) * k is Relation-like D -defined rng x -valued Function-like finite Element of K37(K38(D,(rng x)))
K38(D,(rng x)) is Relation-like finite set
K37(K38(D,(rng x))) is non empty finite V38() set
f * ((id (rng x)) * k) is Relation-like NAT -defined rng x -valued Function-like finite set
D is finite set
M is finite set
K38(D,M) is Relation-like finite set
K37(K38(D,M)) is non empty finite V38() set
card D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
card M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k is Relation-like D -defined M -valued Function-like quasi_total finite Element of K37(K38(D,M))
rng k is finite set
D is set
card D is V6() V7() V8() cardinal set
M is set
K38(M,D) is Relation-like set
K37(K38(M,D)) is non empty set
card M is V6() V7() V8() cardinal set
k is Relation-like M -defined D -valued Function-like quasi_total Element of K37(K38(M,D))
dom k is set
f is set
x is set
k . f is set
k . x is set
k .: (dom k) is set
rng k is set
card (rng k) is V6() V7() V8() cardinal set
D is set
card D is V6() V7() V8() cardinal set
M is set
K38(D,M) is Relation-like set
K37(K38(D,M)) is non empty set
card M is V6() V7() V8() cardinal set
k is Relation-like D -defined M -valued Function-like quasi_total Element of K37(K38(D,M))
dom k is set
rng k is set
f is set
x is set
k . x is set
D is non empty set
M is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len M) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
k is Element of D
<*k*> is Relation-like NAT -defined D -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of D
[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 D -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of D
(M ^ <*k*>) /. ((len M) + 1) is Element of D
len (M ^ <*k*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
len <*k*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len M) + (len <*k*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
dom (M ^ <*k*>) is non empty finite Element of K37(NAT)
(M ^ <*k*>) . ((len M) + 1) is set
D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M is non empty set
k is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
dom k is finite Element of K37(NAT)
f is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
k ^ f is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(k ^ f) /. D is Element of M
k /. D is Element of M
dom (k ^ f) is finite Element of K37(NAT)
(k ^ f) . D is set
k . D is set
D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M is non empty set
f is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
dom f is finite Element of K37(NAT)
k is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
k ^ f 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
(len k) + D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(k ^ f) /. ((len k) + D) is Element of M
f /. D is Element of M
dom (k ^ f) is finite Element of K37(NAT)
(k ^ f) . ((len k) + D) is set
f . D is set
D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
k is set
f is Relation-like NAT -defined k -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of k
f | M is Relation-like NAT -defined k -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of k
Seg M is finite 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 <= M ) } is set
f | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined k -valued Function-like finite FinSubsequence-like set
dom (f | M) is finite Element of K37(NAT)
(f | M) /. D is Element of k
f /. D is Element of k
dom f is finite Element of K37(NAT)
(dom f) /\ (Seg M) is finite Element of K37(NAT)
f | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined k -valued Function-like finite FinSubsequence-like Element of K37(K38(NAT,k))
K38(NAT,k) is Relation-like set
K37(K38(NAT,k)) is non empty set
(f | (Seg M)) . D is set
f . D is set
D is set
M is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
dom 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
M | k is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
M | (Seg k) is Relation-like NAT -defined Seg k -defined NAT -defined D -valued Function-like finite FinSubsequence-like set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(M | k) /. f is Element of D
M /. f is Element of D
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len M) is finite len 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 M ) } is set
(dom M) /\ (Seg k) is finite Element of K37(NAT)
dom (M | k) is finite Element of K37(NAT)
(M | k) . f is set
M . f is set
D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M is finite set
card M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
K37(M) is non empty finite V38() set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng k is finite set
Seg D is finite 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 <= D ) } is set
k | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like finite FinSubsequence-like set
len 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
rng f is finite set
x is finite Element of K37(M)
card x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D is set
M is Relation-like Function-like set
rng M is set
Coim (M,D) is set
{D} is non empty V19() finite 1 -element set
M " {D} is set
card (Coim (M,D)) is V6() V7() V8() cardinal set
D is set
M is set
k is set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
f is 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
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
3 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
x is set
<*f,x*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M,k*> ^ <*f,x*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
3 + 2 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D is set
M is set
k is set
f is set
(D,M,k,f) is set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 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
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
x is set
(D,M,k,f,x) is set
<*f,x*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M,k*> ^ <*f,x*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
D is set
M is set
k is set
f is set
(D,M,k,f) is Relation-like Function-like non empty set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 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
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
x is set
(D,M,k,f,x) is Relation-like Function-like non empty set
<*f,x*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M,k*> ^ <*f,x*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
D is non empty set
M is Element of D
k is Element of D
f is Element of D
x is Element of D
(M,k,f,x) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*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
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*M,k,f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
(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
<*x*> is Relation-like NAT -defined D -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,M,k,f) ^ <*x*> is Relation-like NAT -defined D -valued Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
M is Element of D
k is Element of D
f is Element of D
x is Element of D
y is Element of D
(M,k,f,x,y) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*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
<*x,y*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*y*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,y] is set
{1,y} is non empty finite set
{{1,y},{1}} is non empty finite V38() set
{[1,y]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*x*> ^ <*y*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*M,k,f*> ^ <*x,y*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
(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
(D,x,y) is Relation-like NAT -defined D -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,M,k,f) ^ (D,x,y) is Relation-like NAT -defined D -valued Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like FinSequence of D
D is set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element set
M is set
<*D,M*> 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
<*D*> ^ <*M*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
k is set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
f is set
(D,M,k,f) is Relation-like NAT -defined Function-like non empty finite 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
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
<*k,f*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M*> ^ <*k,f*> is Relation-like NAT -defined Function-like non empty finite 2 + 2 -element FinSequence-like FinSubsequence-like set
2 + 2 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
<*M,k,f*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*M*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 3 -element FinSequence-like FinSubsequence-like set
1 + 3 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
((<*D*> ^ <*M*>) ^ <*k*>) ^ <*f*> is Relation-like NAT -defined Function-like non empty finite ((1 + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((1 + 1) + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
<*M*> ^ <*k,f*> is Relation-like NAT -defined Function-like non empty finite 1 + 2 -element FinSequence-like FinSubsequence-like set
1 + 2 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
<*D*> ^ (<*M*> ^ <*k,f*>) is Relation-like NAT -defined Function-like non empty finite 1 + (1 + 2) -element FinSequence-like FinSubsequence-like set
1 + (1 + 2) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D is set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element set
M is 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
k is set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
f is set
(D,M,k,f) is Relation-like NAT -defined Function-like non empty finite 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
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
((<*D*> ^ <*M*>) ^ <*k*>) ^ <*f*> is Relation-like NAT -defined Function-like non empty finite ((1 + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((1 + 1) + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
x is set
(D,M,k,f,x) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*f,x*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M,k*> ^ <*f,x*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
(D,M,k,f) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(((<*D*> ^ <*M*>) ^ <*k*>) ^ <*f*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite (((1 + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
(((1 + 1) + 1) + 1) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
<*k,f,x*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
(<*k*> ^ <*f*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
<*D,M*> ^ <*k,f,x*> is Relation-like NAT -defined Function-like non empty finite 2 + 3 -element FinSequence-like FinSubsequence-like set
2 + 3 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(M,k,f,x) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*M,k,f*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*M*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
(<*M*> ^ <*k*>) ^ <*f*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
<*M,k,f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
<*D*> ^ (M,k,f,x) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*D,M*> ^ (<*k*> ^ <*f*>) is Relation-like NAT -defined Function-like non empty finite 2 + (1 + 1) -element FinSequence-like FinSubsequence-like set
2 + (1 + 1) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(<*D,M*> ^ (<*k*> ^ <*f*>)) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite (2 + (1 + 1)) + 1 -element FinSequence-like FinSubsequence-like set
(2 + (1 + 1)) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
<*M*> ^ <*k,f,x*> is Relation-like NAT -defined Function-like non empty finite 1 + 3 -element FinSequence-like FinSubsequence-like set
1 + 3 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
<*D*> ^ (<*M*> ^ <*k,f,x*>) is Relation-like NAT -defined Function-like non empty finite 1 + (1 + 3) -element FinSequence-like FinSubsequence-like set
1 + (1 + 3) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
D is set
M is set
k is set
f is set
(D,M,k,f) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 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
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
x . 1 is set
x . 2 is set
x . 3 is set
x . 4 is set
len <*D,M,k*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
len <*f*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len <*D,M,k*>) + (len <*f*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
3 + (len <*f*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
3 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
dom <*D,M,k*> is non empty finite 3 -element Element of K37(NAT)
<*D,M,k*> . 1 is set
<*D,M,k*> . 2 is set
<*D,M,k*> . 3 is set
dom <*f*> is non empty V19() finite 1 -element Element of K37(NAT)
(<*D,M,k*> ^ <*f*>) . (3 + 1) is set
(len <*D,M,k*>) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(<*D,M,k*> ^ <*f*>) . ((len <*D,M,k*>) + 1) is set
<*f*> . 1 is set
dom <*D,M,k*> is non empty finite 3 -element Element of K37(NAT)
len <*D,M,k*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
x . y is set
<*D,M,k*> . y is set
dom <*f*> is non empty V19() finite 1 -element Element of K37(NAT)
len <*D,M,k*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len <*D,M,k*>) + y is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
x . ((len <*D,M,k*>) + y) is set
<*f*> . y is set
3 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
x . (3 + 1) is set
dom x is finite Element of K37(NAT)
3 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg (3 + 1) is non empty finite 3 + 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 <= 3 + 1 ) } is set
(len <*D,M,k*>) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg ((len <*D,M,k*>) + 1) is non empty finite (len <*D,M,k*>) + 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 <= (len <*D,M,k*>) + 1 ) } is set
len <*f*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len <*D,M,k*>) + (len <*f*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg ((len <*D,M,k*>) + (len <*f*>)) is non empty finite (len <*D,M,k*>) + (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 <*D,M,k*>) + (len <*f*>) ) } is set
D is set
M is set
k is set
f is set
x is set
(D,M,k,f,x) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
<*f,x*> is Relation-like NAT -defined Function-like non empty finite 2 -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
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M,k*> ^ <*f,x*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y . 1 is set
y . 2 is set
y . 3 is set
y . 4 is set
y . 5 is set
(D,M,k,f) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
dom <*x*> is non empty V19() finite 1 -element Element of K37(NAT)
(D,M,k,f) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len ((D,M,k,f) ^ <*x*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
len (D,M,k,f) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
len <*x*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len (D,M,k,f)) + (len <*x*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
4 + (len <*x*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
4 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
dom (D,M,k,f) is non empty finite Element of K37(NAT)
(D,M,k,f) . 1 is set
(D,M,k,f) . 2 is set
(D,M,k,f) . 3 is set
(D,M,k,f) . 4 is set
((D,M,k,f) ^ <*x*>) . (4 + 1) is set
(len (D,M,k,f)) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
((D,M,k,f) ^ <*x*>) . ((len (D,M,k,f)) + 1) is set
<*x*> . 1 is set
dom (D,M,k,f) is non empty finite Element of K37(NAT)
len (D,M,k,f) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
y . a is set
(D,M,k,f) . a is set
dom <*x*> is non empty V19() finite 1 -element Element of K37(NAT)
len (D,M,k,f) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
a is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len (D,M,k,f)) + a is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
y . ((len (D,M,k,f)) + a) is set
<*x*> . a is set
4 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
y . (4 + 1) is set
dom y is finite Element of K37(NAT)
4 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg (4 + 1) is non empty finite 4 + 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 <= 4 + 1 ) } is set
(len (D,M,k,f)) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg ((len (D,M,k,f)) + 1) is non empty finite (len (D,M,k,f)) + 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 <= (len (D,M,k,f)) + 1 ) } is set
len <*x*> is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
(len (D,M,k,f)) + (len <*x*>) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg ((len (D,M,k,f)) + (len <*x*>)) is non empty finite (len (D,M,k,f)) + (len <*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 <= (len (D,M,k,f)) + (len <*x*>) ) } is set
(D,M,k,f) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
D is non empty set
M is Element of D
k is Element of D
f is Element of D
x is Element of D
(D,M,k,f,x) is Relation-like NAT -defined D -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence 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
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*M,k,f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
(D,M,k,f,x) /. 1 is Element of D
(D,M,k,f,x) /. 2 is Element of D
(D,M,k,f,x) /. 3 is Element of D
(D,M,k,f,x) /. 4 is Element of D
(D,M,k,f,x) . 2 is set
(D,M,k,f,x) . 3 is set
(D,M,k,f,x) . 4 is set
dom (D,M,k,f,x) is non empty finite Element of K37(NAT)
(D,M,k,f,x) . 1 is set
D is non empty set
M is Element of D
k is Element of D
f is Element of D
x is Element of D
y is Element of D
(D,M,k,f,x,y) is Relation-like NAT -defined D -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence 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
<*x,y*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*y*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,y] is set
{1,y} is non empty finite set
{{1,y},{1}} is non empty finite V38() set
{[1,y]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*x*> ^ <*y*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*M,k,f*> ^ <*x,y*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
(D,M,k,f,x,y) /. 1 is Element of D
(D,M,k,f,x,y) /. 2 is Element of D
(D,M,k,f,x,y) /. 3 is Element of D
(D,M,k,f,x,y) /. 4 is Element of D
(D,M,k,f,x,y) /. 5 is Element of D
(D,M,k,f,x,y) . 4 is set
(D,M,k,f,x,y) . 5 is set
(D,M,k,f,x,y) . 2 is set
(D,M,k,f,x,y) . 3 is set
dom (D,M,k,f,x,y) is non empty finite Element of K37(NAT)
(D,M,k,f,x,y) . 1 is set
F2() is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
Seg F2() is finite F2() -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 <= F2() ) } is set
F1() is non empty set
M is set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
f is Element of F1()
x is set
y is set
D is set
M is Relation-like Function-like set
dom M is set
rng M is set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined F1() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F1()
len f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
f /. x is Element of F1()
f . x is set
D is non empty set
M is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
k is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
dom M is finite Element of K37(NAT)
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len M) is finite len 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 M ) } is set
dom k is finite Element of K37(NAT)
len k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of 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
(len k) - (len 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
x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(len M) + x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k /. ((len M) + x) is Element of D
x is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
len x is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
M ^ x is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
len (M ^ x) is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
(len M) + f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
y is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
(M ^ x) . y is set
M . y is set
k . y is set
y - (len M) is ext-real V31() V32() V33() set
(len M) + (len x) 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 Element of NAT
((len M) + (len x)) - (len M) is ext-real V31() V32() V33() set
0 + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
Seg (len x) is finite len 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 <= len x ) } is set
dom x is finite Element of K37(NAT)
(M ^ x) . y is set
x . y9 is set
x /. y9 is Element of D
(len M) + y9 is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k /. ((len M) + y9) is Element of D
k . y is set
D is non empty set
M is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
k is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
len M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
k . f is set
M . f is set
x is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
M ^ x is Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D
F1() is non empty set
F2() is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
D is Relation-like NAT -defined F1() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F1()
len D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
dom D is finite Element of K37(NAT)
M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
D /. M is Element of F1()
F3(M) is Element of F1()
D . M is set
D is set
M is set
k is set
f is set
(D,M,k,f) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*D,M,k*> is Relation-like NAT -defined Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like set
<*D*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V38() set
{[1,D]} is Relation-like Function-like constant non empty V19() finite 1 -element 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*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like 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
(<*D*> ^ <*M*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite (1 + 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
<*D,M,k*> ^ <*f*> is Relation-like NAT -defined Function-like non empty finite 3 + 1 -element FinSequence-like FinSubsequence-like set
x is set
(D,M,k,f,x) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*f,x*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V38() set
{[1,x]} is Relation-like Function-like constant non empty V19() finite 1 -element set
<*f*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*D,M,k*> ^ <*f,x*> is Relation-like NAT -defined Function-like non empty finite 3 + 2 -element FinSequence-like FinSubsequence-like set
M is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
D is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
D + k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
f is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal Element of NAT
D + f 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
D is set
M is non empty set
K38(D,M) is Relation-like set
K37(K38(D,M)) is non empty set
k is non empty set
K38(M,k) is Relation-like non empty set
K37(K38(M,k)) is non empty set
f is Relation-like D -defined M -valued Function-like total quasi_total Element of K37(K38(D,M))
x is Relation-like M -defined k -valued Function-like non empty total quasi_total Element of K37(K38(M,k))
x * f is Relation-like D -defined k -valued Function-like total quasi_total Element of K37(K38(D,k))
K38(D,k) is Relation-like set
K37(K38(D,k)) is non empty set
dom x is non empty set
rng x is non empty set
rng f is set
rng (x * f) is set
D is set
K38(D,D) is Relation-like set
K37(K38(D,D)) is non empty set
M is Relation-like D -defined D -valued total quasi_total V48() V50() V55() Element of K37(K38(D,D))
Class M is with_non-empty_elements a_partition of D
k is Relation-like D -defined D -valued total quasi_total V48() V50() V55() Element of K37(K38(D,D))
Class k is with_non-empty_elements a_partition of D
f is set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty V19() finite 1 -element set
{{x,y},{x}} is non empty finite V38() set
a is Element of D
Class (M,a) is Element of K37(D)
K37(D) is non empty set
{a} is non empty V19() finite 1 -element set
M .: {a} is set
CE1a is set
Class (k,CE1a) is Element of K37(D)
{CE1a} is non empty V19() finite 1 -element set
k .: {CE1a} is set
[a,CE1a] is set
{a,CE1a} is non empty finite set
{{a,CE1a},{a}} is non empty finite V38() set
[CE1a,a] is set
{CE1a,a} is non empty finite set
{{CE1a,a},{CE1a}} is non empty finite V38() set
y9 is Element of D
[y9,CE1a] is set
{y9,CE1a} is non empty finite set
{y9} is non empty V19() finite 1 -element set
{{y9,CE1a},{y9}} is non empty finite V38() set
x is set
y is set
[x,y] is set
{x,y} is non empty finite set
{x} is non empty V19() finite 1 -element set
{{x,y},{x}} is non empty finite V38() set
a is Element of D
Class (k,a) is Element of K37(D)
{a} is non empty V19() finite 1 -element set
k .: {a} is set
CE1a is set
Class (M,CE1a) is Element of K37(D)
{CE1a} is non empty V19() finite 1 -element set
M .: {CE1a} is set
[a,CE1a] is set
{a,CE1a} is non empty finite set
{{a,CE1a},{a}} is non empty finite V38() set
[CE1a,a] is set
{CE1a,a} is non empty finite set
{{CE1a,a},{CE1a}} is non empty finite V38() set
y9 is Element of D
[y9,CE1a] is set
{y9,CE1a} is non empty finite set
{y9} is non empty V19() finite 1 -element set
{{y9,CE1a},{y9}} is non empty finite V38() set
D is finite set
M is finite V38() with_non-empty_elements a_partition of D
D is non empty finite set
the non empty finite V38() with_non-empty_elements a_partition of D is non empty finite V38() with_non-empty_elements a_partition of D
D is non empty set
M is non empty with_non-empty_elements a_partition of D
k is set
K37(D) is non empty set
f is Element of M
the Element of f is Element of f
y is Element of D
D is non empty finite set
card D is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
M is non empty finite V38() with_non-empty_elements a_partition of D
card M is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
card (card D) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
card (card M) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
proj M is Relation-like D -defined M -valued Function-like non empty total quasi_total finite Element of K37(K38(D,M))
K38(D,M) is Relation-like non empty finite set
K37(K38(D,M)) is non empty finite V38() set
k is set
K37(D) is non empty finite V38() set
f is finite Element of M
x is Element of D
(proj M) . x is finite Element of M
y is finite Element of M
D is non empty finite set
M is non empty finite V38() with_non-empty_elements a_partition of D
card M is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
k is non empty finite V38() with_non-empty_elements a_partition of D
card k is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
f is set
K38(M,k) is Relation-like non empty finite set
K37(K38(M,k)) is non empty finite V38() set
f is Relation-like M -defined k -valued Function-like non empty total quasi_total finite Element of K37(K38(M,k))
card (card M) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
card (card k) is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
x is set
K37(D) is non empty finite V38() set
y is finite Element of k
y9 is Element of D
proj M is Relation-like D -defined M -valued Function-like non empty total quasi_total finite Element of K37(K38(D,M))
K38(D,M) is Relation-like non empty finite set
K37(K38(D,M)) is non empty finite V38() set
(proj M) . y9 is finite Element of M
f . ((proj M) . y9) is finite Element of k
a is finite Element of k
D is non empty finite set
K37(D) is non empty finite V38() set
M is non empty finite V38() with_non-empty_elements a_partition of D
k is non empty finite V38() with_non-empty_elements a_partition of D
f is finite Element of k
K38(D,D) is Relation-like non empty finite set
K37(K38(D,D)) is non empty finite V38() set
x is Relation-like D -defined D -valued total quasi_total finite V48() V50() V55() Element of K37(K38(D,D))
Class x is non empty finite V38() with_non-empty_elements a_partition of D
y9 is Relation-like D -defined D -valued total quasi_total finite V48() V50() V55() Element of K37(K38(D,D))
Class y9 is non empty finite V38() with_non-empty_elements a_partition of D
y is finite Element of K37(D)
a is set
Class (y9,a) is finite Element of K37(D)
{a} is non empty V19() finite 1 -element set
y9 .: {a} is set
Class (x,a) is finite Element of K37(D)
x .: {a} is set
CE1a is finite Element of M
fCE1a is set
p229 is finite Element of K37(D)
c12 is set
Class (y9,c12) is finite Element of K37(D)
{c12} is non empty V19() finite 1 -element set
y9 .: {c12} is set
D is non empty finite set
M is non empty finite V38() with_non-empty_elements a_partition of D
card M is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
k is non empty finite V38() with_non-empty_elements a_partition of D
card k is V6() V7() V8() V12() non empty ext-real positive non negative V31() V32() V33() finite cardinal Element of NAT
f is set
K38(M,k) is Relation-like non empty finite set
K37(K38(M,k)) is non empty finite V38() set
f is Relation-like M -defined k -valued Function-like non empty total quasi_total finite Element of K37(K38(M,k))
dom f is non empty finite set
rng f is non empty finite set
x is set
K37(D) is non empty finite V38() set
y is finite Element of k
y9 is finite Element of M
f . y9 is finite Element of k
CE1a is Element of D
a is finite Element of K37(D)
K37(D) is non empty finite V38() set
x is finite Element of M
f . x is finite Element of k
K38(D,D) is Relation-like non empty finite set
K37(K38(D,D)) is non empty finite V38() set
y9 is Relation-like D -defined D -valued total quasi_total finite V48() V50() V55() Element of K37(K38(D,D))
Class y9 is non empty finite V38() with_non-empty_elements a_partition of D
a is set
y is finite Element of K37(D)
Class (y9,a) is finite Element of K37(D)
{a} is non empty V19() finite 1 -element set
y9 .: {a} is set
CE1a is finite Element of M
f . CE1a is finite Element of k
fCE1a is finite Element of K37(D)
x is set
y is finite Element of M
f . y is finite Element of k
y is set
f . y is set
y9 is finite Element of M
f . y9 is finite Element of k
D is set
D * is functional non empty FinSequence-membered set
M is Relation-like NAT -defined D * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D *
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M /. k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of D *
D is set
D * is functional non empty FinSequence-membered set
M is Relation-like NAT -defined D * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of D *
k is V6() V7() V8() V12() ext-real non negative V31() V32() V33() finite cardinal set
M /. k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of D *
f is Relation-like Function-like set