:: FINSEQ_6 semantic presentation

REAL is set
NAT is non empty V7() V8() V9() V34() cardinal limit_cardinal Element of bool REAL
bool REAL is set
NAT is non empty V7() V8() V9() V34() cardinal limit_cardinal set
bool NAT is V34() set
bool NAT is V34() set
COMPLEX is set
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is Relation-like V34() set
[:[:NAT,NAT:],NAT:] is Relation-like V34() set
bool [:[:NAT,NAT:],NAT:] is V34() set
K266() is set
1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
{} is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
3 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial V34() 1 -element Element of bool NAT
{1} is non empty trivial 1 -element set
Seg 2 is non empty V34() 2 -element Element of bool NAT
{1,2} is non empty set
dom {} is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
rng {} is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
D is set
f is set
k1 is set
<*D,f,k1*> is non empty Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
len <*D,f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom D is non empty Element of bool NAT
D is set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
rng <*D,f*> is non empty set
{D,f} is non empty set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
<*D*> ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng <*D*> is non empty trivial 1 -element set
rng <*f*> is non empty trivial 1 -element set
(rng <*D*>) \/ (rng <*f*>) is non empty set
{D} is non empty trivial 1 -element set
{D} \/ (rng <*f*>) is non empty set
{f} is non empty trivial 1 -element set
{D} \/ {f} is non empty set
D is set
f is set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
rng <*D,f,k1*> is non empty set
{D,f,k1} is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
<*k1*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
<*D,f*> ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() 2 + 1 -element FinSequence-like FinSubsequence-like set
2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng <*D,f*> is non empty set
rng <*k1*> is non empty trivial 1 -element set
(rng <*D,f*>) \/ (rng <*k1*>) is non empty set
{D,f} is non empty set
{D,f} \/ (rng <*k1*>) is non empty set
{k1} is non empty trivial 1 -element set
{D,f} \/ {k1} is non empty set
D is set
Sgm D is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm D) . 1 is set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
Seg f is V34() f -element Element of bool NAT
len (Sgm D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (Sgm D) is Element of bool NAT
rng (Sgm D) is set
k2 is set
(Sgm D) . k2 is set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom f is Element of bool NAT
f . D is set
(f . D) .. f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng f is set
f . ((f . D) .. f) is set
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
<*D,f*> | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined Function-like FinSubsequence-like set
len <*D,f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,f*> is non empty non trivial 2 -element Element of bool NAT
dom (<*D,f*> | (Seg 1)) is Element of bool NAT
(dom <*D,f*>) /\ (Seg 1) is Element of bool NAT
k2 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom k2 is Element of bool NAT
k2 . 1 is set
<*D,f*> . 1 is set
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
f is set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
<*D,f,k1*> | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined Function-like FinSubsequence-like set
len <*D,f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,f,k1*> is non empty non trivial 3 -element Element of bool NAT
dom (<*D,f,k1*> | (Seg 1)) is Element of bool NAT
(dom <*D,f,k1*>) /\ (Seg 1) is Element of bool NAT
i is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom i is Element of bool NAT
i . 1 is set
<*D,f,k1*> . 1 is set
len i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
<*D,f,k1*> | (Seg 2) is Relation-like NAT -defined Seg 2 -defined NAT -defined Function-like FinSubsequence-like set
len <*D,f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,f,k1*> is non empty non trivial 3 -element Element of bool NAT
dom (<*D,f,k1*> | (Seg 2)) is Element of bool NAT
(dom <*D,f,k1*>) /\ (Seg 2) is Element of bool NAT
i is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom i is Element of bool NAT
i . 2 is set
<*D,f,k1*> . 2 is set
i . 1 is set
<*D,f,k1*> . 1 is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is set
k1 .. (D ^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
dom (D ^ f) is Element of bool NAT
(D ^ f) . (k1 .. D) is set
D . (k1 .. D) is set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D ^ f) . k2 is set
D . k2 is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng f is set
(rng D) \ (rng f) is Element of bool (rng D)
bool (rng D) is set
f ^ D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is set
k1 .. (f ^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + (k1 .. D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
D . (k1 .. D) is set
(f ^ D) . ((len f) + (k1 .. D)) is set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom f is Element of bool NAT
(f ^ D) . k2 is set
f . k2 is set
k2 - (len f) is ext-real V14() V32() V33() Element of REAL
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i + (len f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f ^ D) . k2 is set
D . i is set
dom (f ^ D) is Element of bool NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is set
(D ^ f) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D |-- k1) ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 .. (D ^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (D |-- k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len D) - (k1 .. D) is ext-real V14() V32() V33() Element of REAL
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom ((D |-- k1) ^ f) is Element of bool NAT
dom (D |-- k1) is Element of bool NAT
(len (D |-- k1)) + (k1 .. D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + (k1 .. D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
((D |-- k1) ^ f) . k2 is set
(D |-- k1) . k2 is set
D . (k2 + (k1 .. D)) is set
k2 + (k1 .. (D ^ f)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D ^ f) . (k2 + (k1 .. (D ^ f))) is set
dom f is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len (D |-- k1)) + i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len (D |-- k1)) + i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((D |-- k1) ^ f) . k2 is set
f . i is set
(len D) + i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D ^ f) . ((len D) + i) is set
k2 + (k1 .. (D ^ f)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D ^ f) . (k2 + (k1 .. (D ^ f))) is set
dom (D |-- k1) is Element of bool NAT
dom f is Element of bool NAT
rng (D ^ f) is set
rng f is set
(rng D) \/ (rng f) is set
len ((D |-- k1) ^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len D) - (k1 .. D)) + (len f) is ext-real V14() V32() V33() Element of REAL
(len D) + (len f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len D) + (len f)) - (k1 .. D) is ext-real V14() V32() V33() Element of REAL
len (D ^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (D ^ f)) - (k1 .. (D ^ f)) is ext-real V14() V32() V33() Element of REAL
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng f is set
(rng D) \ (rng f) is Element of bool (rng D)
bool (rng D) is set
f ^ D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is set
(f ^ D) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + (k1 .. D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 .. (f ^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k2 + (k1 .. D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (D |-- k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len D) - (k1 .. D) is ext-real V14() V32() V33() Element of REAL
(len (D |-- k1)) + (k1 .. D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (D |-- k1) is Element of bool NAT
dom D is Element of bool NAT
(D |-- k1) . k2 is set
D . (k2 + (k1 .. D)) is set
(len f) + (k2 + (k1 .. D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f ^ D) . ((len f) + (k2 + (k1 .. D))) is set
k2 + (k1 .. (f ^ D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f ^ D) . (k2 + (k1 .. (f ^ D))) is set
rng (f ^ D) is set
(rng f) \/ (rng D) is set
(len f) + (len D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) + (len D)) - ((len f) + (k1 .. D)) is ext-real V14() V32() V33() Element of REAL
len (f ^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (f ^ D)) - (k1 .. (f ^ D)) is ext-real V14() V32() V33() Element of REAL
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom D is Element of bool NAT
k1 is set
D . k1 is set
(D ^ f) . k1 is set
dom (D ^ f) is Element of bool NAT
k1 is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom D is Element of bool NAT
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D ^ f) | k1 is Relation-like NAT -defined k1 -defined NAT -defined Function-like FinSubsequence-like set
D | k1 is Relation-like NAT -defined k1 -defined NAT -defined Function-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is set
(D ^ f) -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 .. D) - 1 is ext-real V14() V32() V33() Element of REAL
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
Seg k2 is V34() k2 -element Element of bool NAT
D | (Seg k2) is Relation-like NAT -defined Seg k2 -defined NAT -defined Function-like FinSubsequence-like set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (len D) is V34() len D -element Element of bool NAT
dom D is Element of bool NAT
(D ^ f) | (Seg k2) is Relation-like NAT -defined Seg k2 -defined NAT -defined Function-like FinSubsequence-like set
rng (D ^ f) is set
rng f is set
(rng D) \/ (rng f) is set
k1 .. (D ^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 .. (D ^ f)) - 1 is ext-real V14() V32() V33() Element of REAL
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
Seg f is V34() f -element Element of bool NAT
D | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined Function-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 ^ D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom (k1 ^ D) is Element of bool NAT
dom (k1 ^ f) is Element of bool NAT
k2 is set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom k1 is Element of bool NAT
dom D is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom f is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len k1) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom k1 is Element of bool NAT
dom D is Element of bool NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is set
(k1 ^ D) . k2 is set
(k1 ^ f) . k2 is set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom k1 is Element of bool NAT
k1 . i is set
dom D is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom f is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len k1) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len k1) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D . k2 is set
f . k2 is set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom k1 is Element of bool NAT
dom D is Element of bool NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len D) + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg ((len D) + k1) is V34() (len D) + k1 -element Element of bool NAT
(D ^ f) | (Seg ((len D) + k1)) is Relation-like NAT -defined Seg ((len D) + k1) -defined NAT -defined Seg ((len D) + k1) -defined Function-like V34() FinSequence-like FinSubsequence-like set
Seg k1 is V34() k1 -element Element of bool NAT
f | (Seg k1) is Relation-like NAT -defined Seg k1 -defined NAT -defined Seg k1 -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ (f | (Seg k1)) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom (D ^ (f | (Seg k1))) is Element of bool NAT
k2 is set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
Seg (len D) is V34() len D -element Element of bool NAT
dom (f | (Seg k1)) is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len D) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len D) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom f is Element of bool NAT
(dom f) /\ (Seg k1) is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
dom (f | (Seg k1)) is Element of bool NAT
dom (D ^ f) is Element of bool NAT
(dom (D ^ f)) /\ (Seg ((len D) + k1)) is Element of bool NAT
k2 is set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
dom f is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len D) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len D) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (f | (Seg k1)) is Element of bool NAT
(dom f) /\ (Seg k1) is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
dom f is Element of bool NAT
dom ((D ^ f) | (Seg ((len D) + k1))) is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom D is Element of bool NAT
((D ^ f) | (Seg ((len D) + k1))) . k2 is set
(D ^ f) . k2 is set
D . k2 is set
(D ^ (f | (Seg k1))) . k2 is set
k2 - (len D) is ext-real V14() V32() V33() Element of REAL
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len D) + i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom D is Element of bool NAT
dom f is Element of bool NAT
dom (f | (Seg k1)) is Element of bool NAT
(dom f) /\ (Seg k1) is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len D) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((D ^ f) | (Seg ((len D) + k1))) . k2 is set
(D ^ f) . k2 is set
f . i is set
(f | (Seg k1)) . i is set
(D ^ (f | (Seg k1))) . k2 is set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len D) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng f is set
(rng D) \ (rng f) is Element of bool (rng D)
bool (rng D) is set
f ^ D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is set
(f ^ D) -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f ^ (D -| k1) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 .. D) - 1 is ext-real V14() V32() V33() Element of REAL
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
Seg k2 is V34() k2 -element Element of bool NAT
D | (Seg k2) is Relation-like NAT -defined Seg k2 -defined NAT -defined Seg k2 -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 .. (f ^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + (k1 .. D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 .. (f ^ D)) - 1 is ext-real V14() V32() V33() Element of REAL
rng (f ^ D) is set
(rng f) \/ (rng D) is set
Seg ((len f) + k2) is V34() (len f) + k2 -element Element of bool NAT
(f ^ D) | (Seg ((len f) + k2)) is Relation-like NAT -defined Seg ((len f) + k2) -defined NAT -defined Seg ((len f) + k2) -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng f is set
(rng D) \+\ (rng f) is set
(rng D) \ (rng f) is set
(rng f) \ (rng D) is set
((rng D) \ (rng f)) \/ ((rng f) \ (rng D)) is set
k1 is set
rng (D ^ f) is set
(rng D) \/ (rng f) is set
(rng D) /\ (rng f) is set
(D ^ f) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D |-- k1) ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng ((D |-- k1) ^ f) is set
rng (D |-- k1) is set
(rng (D |-- k1)) \/ (rng f) is set
((rng D) \/ (rng f)) \ ((rng D) /\ (rng f)) is Element of bool ((rng D) \/ (rng f))
bool ((rng D) \/ (rng f)) is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is set
(D ^ f) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D |-- k1) ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng ((D ^ f) |-- k1) is set
rng (D |-- k1) is set
rng f is set
(rng (D |-- k1)) \/ (rng f) is set
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
D .. <*D*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D*> . 1 is set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
<*D*> . f is set
dom <*D*> is non empty trivial 1 -element Element of bool NAT
D is set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
D .. <*D,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f*> . 1 is set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
<*D,f*> . k1 is set
len <*D,f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,f*> is non empty non trivial 2 -element Element of bool NAT
D is set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
f .. <*D,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f*> . 2 is set
<*D,f*> . 1 is set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f*> . k1 is set
len <*D,f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,f*> is non empty non trivial 2 -element Element of bool NAT
D is set
f is set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
D .. <*D,f,k1*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f,k1*> . 1 is set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
<*D,f,k1*> . k2 is set
len <*D,f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,f,k1*> is non empty non trivial 3 -element Element of bool NAT
D is set
f is set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
f .. <*D,f,k1*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f,k1*> . 2 is set
<*D,f,k1*> . 1 is set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f,k1*> . k2 is set
len <*D,f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,f,k1*> is non empty non trivial 3 -element Element of bool NAT
D is set
f is set
k1 is set
<*D,k1,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
f .. <*D,k1,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,k1,f*> . 3 is set
<*D,k1,f*> . 1 is set
<*D,k1,f*> . 2 is set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,k1,f*> . k2 is set
len <*D,k1,f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom <*D,k1,f*> is non empty non trivial 3 -element Element of bool NAT
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> ^ f is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (<*D*> ^ f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev f) ^ <*D*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev <*D*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev f) ^ (Rev <*D*>) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (Rev D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
<*D,f*> -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f .. <*D,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f .. <*D,f*>) - 1 is ext-real V14() V32() V33() Element of REAL
rng <*D,f*> is non empty set
{D,f} is non empty set
<*D,f*> | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined Seg 1 -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
f is set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
<*D,f,k1*> -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f .. <*D,f,k1*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f .. <*D,f,k1*>) - 1 is ext-real V14() V32() V33() Element of REAL
rng <*D,f,k1*> is non empty set
{D,f,k1} is set
<*D,f,k1*> | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined Seg 1 -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is set
f is set
k1 is set
<*D,k1,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
<*D,k1,f*> -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
rng <*D,k1,f*> is non empty set
{D,k1,f} is set
f .. <*D,k1,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f .. <*D,k1,f*>) - 1 is ext-real V14() V32() V33() Element of REAL
<*D,k1,f*> | (Seg 2) is Relation-like NAT -defined Seg 2 -defined NAT -defined Seg 2 -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
<*D,f*> |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
D .. <*D,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*f*>) + (D .. <*D,f*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*D,f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*D,f*>) - (D .. <*D,f*>) is ext-real V14() V32() V33() Element of REAL
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom <*f*> is non empty trivial 1 -element Element of bool NAT
<*f*> . k1 is set
k1 + (D .. <*D,f*>) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f*> . (k1 + (D .. <*D,f*>)) is set
{D,f} is non empty set
rng <*D,f*> is non empty set
D is set
f is set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
<*D,f,k1*> |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
f .. <*D,f,k1*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*k1*>) + (f .. <*D,f,k1*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*D,f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*D,f,k1*>) - (f .. <*D,f,k1*>) is ext-real V14() V32() V33() Element of REAL
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom <*k1*> is non empty trivial 1 -element Element of bool NAT
<*k1*> . k2 is set
k2 + (f .. <*D,f,k1*>) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f,k1*> . (k2 + (f .. <*D,f,k1*>)) is set
{D,f,k1} is set
rng <*D,f,k1*> is non empty set
D is set
f is set
k1 is set
<*D,f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
<*D,f,k1*> |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f,k1*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
D .. <*D,f,k1*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*f,k1*>) + (D .. <*D,f,k1*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*D,f,k1*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*D,f,k1*>) - (D .. <*D,f,k1*>) is ext-real V14() V32() V33() Element of REAL
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom <*f,k1*> is non empty non trivial 2 -element Element of bool NAT
<*f,k1*> . k2 is set
k2 + (D .. <*D,f,k1*>) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f,k1*> . (k2 + (D .. <*D,f,k1*>)) is set
<*f,k1*> . k2 is set
k2 + (D .. <*D,f,k1*>) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*D,f,k1*> . (k2 + (D .. <*D,f,k1*>)) is set
{D,f,k1} is set
rng <*D,f,k1*> is non empty set
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
<*D*> |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> -| D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
{D} is non empty trivial 1 -element set
rng <*D*> is non empty trivial 1 -element set
D .. <*D*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is set
f is set
<*D,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 2 -element FinSequence-like FinSubsequence-like set
<*D,f*> |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
{D,f} is non empty set
rng <*D,f*> is non empty set
f .. <*D,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*D,f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is set
f is set
k1 is set
<*D,k1,f*> is non empty non trivial Relation-like NAT -defined Function-like V34() 3 -element FinSequence-like FinSubsequence-like set
<*D,k1,f*> |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len <*D,k1,f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
{D,k1,f} is set
rng <*D,k1,f*> is non empty set
f .. <*D,k1,f*> is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is set
f is set
k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng k1 is set
k1 -| D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k1 -| D) is set
(k1 -| D) -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
(k1 -| D) ^ <*D*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((k1 -| D) ^ <*D*>) ^ (k1 |-- D) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(((k1 -| D) ^ <*D*>) ^ (k1 |-- D)) -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> ^ (k1 |-- D) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k1 -| D) ^ (<*D*> ^ (k1 |-- D)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((k1 -| D) ^ (<*D*> ^ (k1 |-- D))) -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng f is set
f ^ <*D*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(f ^ <*D*>) ^ k1 is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D .. ((f ^ <*D*>) ^ k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
{D} is non empty trivial 1 -element set
rng <*D*> is non empty trivial 1 -element set
(rng <*D*>) \ (rng f) is Element of bool (rng <*D*>)
bool (rng <*D*>) is set
(f ^ <*D*>) |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (f ^ <*D*>) is non empty set
(rng f) \/ (rng <*D*>) is non empty set
len (f ^ <*D*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D .. (f ^ <*D*>) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (f ^ <*D*>)) - (D .. (f ^ <*D*>)) is ext-real V14() V32() V33() Element of REAL
len ((f ^ <*D*>) |-- D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + (len <*D*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D .. f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Rev f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D .. (Rev f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D .. f) + (D .. (Rev f)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng f is set
f -| D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
(f -| D) ^ <*D*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((f -| D) ^ <*D*>) ^ (f |-- D) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len ((f -| D) ^ <*D*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (f |-- D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len ((f -| D) ^ <*D*>)) + (len (f |-- D)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (f -| D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (f -| D)) + (len <*D*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len (f -| D)) + (len <*D*>)) + (len (f |-- D)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (f -| D)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len (f -| D)) + 1) + (len (f |-- D)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng (f |-- D) is set
Rev (f |-- D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (Rev (f |-- D)) is set
Rev ((f -| D) ^ <*D*>) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev (f |-- D)) ^ (Rev ((f -| D) ^ <*D*>)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (f -| D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> ^ (Rev (f -| D)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev (f |-- D)) ^ (<*D*> ^ (Rev (f -| D))) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev (f |-- D)) ^ <*D*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((Rev (f |-- D)) ^ <*D*>) ^ (Rev (f -| D)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len (Rev (f |-- D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (Rev (f |-- D))) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D .. f) - 1 is ext-real V14() V32() V33() Element of REAL
((D .. f) - 1) + 1 is ext-real V14() V32() V33() Element of REAL
((len (f -| D)) + 1) + (len (Rev (f |-- D))) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((len (f -| D)) + 1) + (len (Rev (f |-- D)))) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f -| D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (f -| D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev f) |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len (Rev (f -| D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (f -| D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng f is set
rng (Rev f) is set
D .. f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D .. (Rev f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D .. f) + (D .. (Rev f)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D .. f) - 1 is ext-real V14() V32() V33() Element of REAL
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
Seg k2 is V34() k2 -element Element of bool NAT
f | (Seg k2) is Relation-like NAT -defined Seg k2 -defined NAT -defined Seg k2 -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom (Rev (f -| D)) is Element of bool NAT
(D .. f) - k1 is ext-real V14() V32() V33() set
dom (f -| D) is Element of bool NAT
k1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 + (D .. (Rev f)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (Rev f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((D .. f) - 1) - k1 is ext-real V14() V32() V33() Element of REAL
(((D .. f) - 1) - k1) + 1 is ext-real V14() V32() V33() Element of REAL
dom (f | (Seg k2)) is Element of bool NAT
dom (Rev f) is Element of bool NAT
(Rev (f -| D)) . k1 is set
(f -| D) . ((((D .. f) - 1) - k1) + 1) is set
(len f) - (k1 + (D .. (Rev f))) is ext-real V14() V32() V33() Element of REAL
((len f) - (k1 + (D .. (Rev f)))) + 1 is ext-real V14() V32() V33() Element of REAL
f . (((len f) - (k1 + (D .. (Rev f)))) + 1) is set
(Rev f) . (k1 + (D .. (Rev f))) is set
(len f) - (D .. (Rev f)) is ext-real V14() V32() V33() Element of REAL
(len (Rev f)) - (D .. (Rev f)) is ext-real V14() V32() V33() Element of REAL
D is set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng f is set
f -| D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (f -| D) is set
Rev (f -| D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (Rev (f -| D)) is set
(Rev f) |-- D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng ((Rev f) |-- D) is set
rng (Rev f) is set
D is non empty set
f is Element of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k1 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 | (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ (k1 /^ (f .. k1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. 1 is Element of D
rng f is set
dom f is Element of bool NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. 1 is Element of D
(f /. 1) .. f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom f is Element of bool NAT
{(f /. 1)} is non empty trivial 1 -element set
f " {(f /. 1)} is Element of bool NAT
f " {(f /. 1)} is set
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (len f) is V34() len f -element Element of bool NAT
Sgm (f " {(f /. 1)}) is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (f " {(f /. 1)})) . 1 is set
D is non empty set
f is Element of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 /. 1 is Element of D
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
{} ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
({} ^ <*f*>) ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ k1) /. 1 is Element of D
dom <*f*> is non empty trivial 1 -element Element of bool NAT
dom (<*f*> ^ k1) is non empty Element of bool NAT
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(<*f*> ^ k1) /. (0 + 1) is Element of D
<*((<*f*> ^ k1) /. (0 + 1))*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*((<*f*> ^ k1) /. (0 + 1))*> ^ ((<*f*> ^ k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ k1) /^ 0 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Element of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*k1*> is non empty Relation-like NAT -defined D -valued Function-like V34() 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Element of D
k2 is Element of D
<*f,k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1,k2*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*k1,k2*> is non empty Relation-like NAT -defined D -valued Function-like V34() 1 + 2 -element FinSequence-like FinSubsequence-like FinSequence of D
1 + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
dom k1 is Element of bool NAT
k1 /. D is Element of f
(k1 /. D) .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng k1 is set
k1 /. ((k1 /. D) .. k1) is Element of f
D is non empty set
f is Element of D
k1 is Element of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*f,k1*> is non empty set
{f,k1} is non empty set
<*f,k1*> -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(<*f,k1*> -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*k1*> is non empty Relation-like NAT -defined D -valued Function-like V34() 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Element of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
k2 is Element of D
<*f,k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1,k2*> -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*f,k1,k2*> is non empty set
{f,k1,k2} is set
<*f,k1,k2*> -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(<*f,k1,k2*> -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*k1*> is non empty Relation-like NAT -defined D -valued Function-like V34() 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Element of D
k2 is Element of D
<*f,k2,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k2,k1*> -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*f,k2,k1*> is non empty set
{f,k2,k1} is set
<*f,k2,k1*> -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(<*f,k2,k1*> -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k2*> ^ <*k1*> is non empty Relation-like NAT -defined D -valued Function-like V34() 2 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f*> :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
{f} is non empty trivial 1 -element set
rng <*f*> is non empty trivial 1 -element set
<*f*> |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (<*f*> |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ {} is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(<*f*> -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
{} ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Element of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
{f,k1} is non empty set
rng <*f,k1*> is non empty set
<*f,k1*> |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ (<*f,k1*> |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ {} is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Element of D
k2 is Element of D
<*f,k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1,k2*> :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
{f,k1,k2} is set
rng <*f,k1,k2*> is non empty set
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1,k2*> |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ (<*f,k1,k2*> |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k2*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> ^ <*k2*> is non empty Relation-like NAT -defined D -valued Function-like V34() 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Element of D
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
k2 is Element of D
<*f,k2,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k2,k1*> :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
{f,k2,k1} is set
rng <*f,k2,k1*> is non empty set
<*f,k2,k1*> |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ (<*f,k2,k1*> |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ {} is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Element of f
k2 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng k2 is set
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
k1 .. (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D + (k1 .. (k2 /^ D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 .. k2) - D is ext-real V14() V32() V33() set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k2) - D is ext-real V14() V32() V33() Element of REAL
D + i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k2 /^ D) is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
D + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k2 /. (D + k2) is Element of f
(k2 /^ D) /. k2 is Element of f
J is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D + J is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom k2 is Element of bool NAT
k2 /. (D + i) is Element of f
(k2 /^ D) /. i is Element of f
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Element of f
k2 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng k2 is set
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng (k2 /^ D) is set
k1 .. (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D + (k1 .. (k2 /^ D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k2) - D is ext-real V14() V32() V33() Element of REAL
(len (k2 /^ D)) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k2 /^ D) is Element of bool NAT
(k2 /^ D) /. (k1 .. (k2 /^ D)) is Element of f
k2 /. (D + (k1 .. (k2 /^ D))) is Element of f
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 is non empty set
k2 is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
dom k2 is Element of bool NAT
k2 /. f is Element of k1
k2 /^ D is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
rng (k2 /^ D) is set
f - D is ext-real V14() V32() V33() set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k2) - D is ext-real V14() V32() V33() Element of REAL
(len (k2 /^ D)) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k2 /^ D) is Element of bool NAT
(k2 /^ D) /. i is Element of k1
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Element of f
k2 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng k2 is set
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
(k2 /^ D) -: k1 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
k2 -: k1 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
(k2 -: k1) /^ D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng (k2 /^ D) is set
k1 .. (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D + (k1 .. (k2 /^ D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len ((k2 /^ D) -: k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 .. k2) - D is ext-real V14() V32() V33() set
len (k2 -: k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (k2 -: k1)) - D is ext-real V14() V32() V33() Element of REAL
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
i + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom ((k2 /^ D) -: k1) is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k2 -: k1) is Element of bool NAT
Seg (k1 .. (k2 /^ D)) is V34() k1 .. (k2 /^ D) -element Element of bool NAT
(k2 /^ D) | (k1 .. (k2 /^ D)) is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
dom (k2 /^ D) is Element of bool NAT
Seg (k1 .. k2) is V34() k1 .. k2 -element Element of bool NAT
((k2 /^ D) -: k1) . i is set
((k2 /^ D) -: k1) /. i is Element of f
(k2 /^ D) /. i is Element of f
k2 /. (i + D) is Element of f
(k2 -: k1) /. (k2 + D) is Element of f
(k2 -: k1) . (i + D) is set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 /^ 1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 :- f) is non empty set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
rng <*f*> is non empty trivial 1 -element set
{f} is non empty trivial 1 -element set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ (k1 /^ (f .. k1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 /^ (f .. k1)) is set
(rng <*f*>) \/ (rng (k1 /^ (f .. k1))) is non empty set
D is set
f is non empty set
k1 is Element of f
k2 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng k2 is set
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 :- k1 is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng (k2 :- k1) is non empty set
<*k1*> is non empty trivial Relation-like NAT -defined f -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of f
k2 /^ (k1 .. k2) is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
<*k1*> ^ (k2 /^ (k1 .. k2)) is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng <*k1*> is non empty trivial 1 -element set
rng (k2 /^ (k1 .. k2)) is set
(rng <*k1*>) \/ (rng (k2 /^ (k1 .. k2))) is non empty set
i is Element of f
k2 . (k1 .. k2) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Element of f
k2 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng k2 is set
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /. D is Element of f
k2 :- k1 is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng (k2 :- k1) is non empty set
dom k2 is Element of bool NAT
k2 is Element of f
k2 /^ (k1 .. k2) is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng (k2 /^ (k1 .. k2)) is set
<*k1*> is non empty trivial Relation-like NAT -defined f -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of f
<*k1*> ^ (k2 /^ (k1 .. k2)) is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng <*k1*> is non empty trivial 1 -element set
(rng <*k1*>) \/ (rng (k2 /^ (k1 .. k2))) is non empty set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 ^ k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 ^ k2) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) ^ k2 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 ^ k2) is set
rng k2 is set
(rng k1) \/ (rng k2) is set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k1 ^ k2) |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ ((k1 ^ k2) |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k1 |-- f) ^ k2 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ ((k1 |-- f) ^ k2) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(<*f*> ^ (k1 |-- f)) ^ k2 is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
(rng k1) \ (rng k2) is Element of bool (rng k1)
bool (rng k1) is set
k2 ^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 ^ k1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 ^ k1) is set
(rng k2) \/ (rng k1) is set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k2 ^ k1) |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ ((k2 ^ k1) |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 ^ k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 ^ k2) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 ^ k2) is set
rng k2 is set
(rng k1) \/ (rng k2) is set
(k1 ^ k2) -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
((k1 ^ k2) -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k1 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
(rng k1) \ (rng k2) is Element of bool (rng k1)
bool (rng k1) is set
k2 ^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 ^ k1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 ^ (k1 -: f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 ^ k1) is set
(rng k2) \/ (rng k1) is set
(k2 ^ k1) -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
((k2 ^ k1) -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 ^ (k1 -| f) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k2 ^ (k1 -| f)) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k1 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 ^ ((k1 -| f) ^ <*f*>) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ (k1 /^ (f .. k1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ (k1 /^ (f .. k1))) /. 1 is Element of D
(<*f*> ^ (k1 /^ (f .. k1))) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Element of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
k2 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: f) is set
(rng k2) \ (rng (k2 -: f)) is Element of bool (rng k2)
bool (rng k2) is set
k2 |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k2 |-- f) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k2 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng ((k2 -| f) ^ <*f*>) is non empty set
((k2 -| f) ^ <*f*>) ^ (k2 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k2 |-- f) is set
(rng ((k2 -| f) ^ <*f*>)) \/ (rng (k2 |-- f)) is non empty set
(rng (k2 |-- f)) \ (rng ((k2 -| f) ^ <*f*>)) is Element of bool (rng (k2 |-- f))
bool (rng (k2 |-- f)) is set
(((k2 -| f) ^ <*f*>) ^ (k2 |-- f)) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 -: f) is set
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 :- f) is non empty set
(rng (k1 -: f)) \/ (rng (k1 :- f)) is non empty set
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k1 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k1 -| f) is set
rng <*f*> is non empty trivial 1 -element set
(rng (k1 -| f)) \/ (rng <*f*>) is non empty set
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k1 |-- f) is set
(rng <*f*>) \/ (rng (k1 |-- f)) is non empty set
((k1 -| f) ^ <*f*>) ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng ((k1 -| f) ^ <*f*>) is non empty set
(rng ((k1 -| f) ^ <*f*>)) \/ (rng (k1 |-- f)) is non empty set
(rng <*f*>) \/ (rng <*f*>) is non empty set
(rng (k1 -| f)) \/ ((rng <*f*>) \/ (rng <*f*>)) is non empty set
((rng (k1 -| f)) \/ ((rng <*f*>) \/ (rng <*f*>))) \/ (rng (k1 |-- f)) is non empty set
((rng (k1 -| f)) \/ (rng <*f*>)) \/ (rng <*f*>) is non empty set
(((rng (k1 -| f)) \/ (rng <*f*>)) \/ (rng <*f*>)) \/ (rng (k1 |-- f)) is non empty set
D is non empty set
f is Element of D
k1 is Element of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
k2 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: f) is set
(rng k2) \ (rng (k2 -: f)) is Element of bool (rng k2)
bool (rng k2) is set
k2 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k2 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k2 -| f) is set
rng <*f*> is non empty trivial 1 -element set
(rng (k2 -| f)) \/ (rng <*f*>) is non empty set
rng (k2 :- f) is non empty set
(rng (k2 -: f)) \/ (rng (k2 :- f)) is non empty set
k2 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (k2 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k2 |-- f) is set
(rng <*f*>) \/ (rng (k2 |-- f)) is non empty set
(rng (k2 |-- f)) \ (rng <*f*>) is Element of bool (rng (k2 |-- f))
bool (rng (k2 |-- f)) is set
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ ((k2 :- f) |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(<*f*> ^ (k2 |-- f)) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ ((<*f*> ^ (k2 |-- f)) |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k2 |-- f) |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ ((k2 |-- f) |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> ^ (k2 |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f .. (k1 -: f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k1 -: f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (f .. k1) is V34() f .. k1 -element Element of bool NAT
(k1 -: f) /. (f .. k1) is Element of D
k1 /. (f .. k1) is Element of D
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(k1 -: f) /. k2 is Element of D
k1 /. k2 is Element of D
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom k1 is Element of bool NAT
dom (k1 -: f) is Element of bool NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
k1 | D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
(k1 | D) | D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
Seg D is V34() D -element Element of bool NAT
k1 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Seg D -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,f:]
[:NAT,f:] is Relation-like V34() set
bool [:NAT,f:] is V34() set
(k1 | (Seg D)) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Seg D -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,f:]
(Seg D) /\ (Seg D) is Element of bool NAT
k1 | ((Seg D) /\ (Seg D)) is Relation-like NAT -defined (Seg D) /\ (Seg D) -defined NAT -defined f -valued Function-like FinSubsequence-like Element of bool [:NAT,f:]
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f .. (k1 -: f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -: f) | (f .. (k1 -: f)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 | (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 | (f .. k1)) | (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Element of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
k2 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: f) is set
(k2 -: f) -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
{f} is non empty trivial 1 -element set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
rng <*f*> is non empty trivial 1 -element set
k2 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k2 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k2 -| f) is set
(rng (k2 -| f)) \/ (rng <*f*>) is non empty set
(k2 -: f) -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: f) -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((k2 -| f) ^ <*f*>) -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(((k2 -| f) ^ <*f*>) -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k2 -| f) -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((k2 -| f) -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k2 -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) ^ ((k1 :- f) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (k1 |-- f) is set
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k1 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((k1 -| f) ^ <*f*>) ^ ((k1 :- f) /^ 1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ k2 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ k2) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k1 -| f) ^ <*f*>) ^ ((<*f*> ^ k2) /^ 1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((k1 -| f) ^ <*f*>) ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f ^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f ^ k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 1) ^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f . 1 is set
k2 is Element of D
<*k2*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
i is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k2*> ^ i is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i ^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k2*> ^ (i ^ k1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*k2*> ^ (i ^ k1)) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 /^ 1) is set
k1 /. 1 is Element of D
<*(k1 /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*(k1 /. 1)*> ^ (k1 /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*(k1 /. 1)*> is non empty trivial 1 -element set
(rng <*(k1 /. 1)*>) \/ (rng (k1 /^ 1)) is non empty set
{(k1 /. 1)} is non empty trivial 1 -element set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f .. (k1 :- f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 :- f) /. 1 is Element of D
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Element of f
k2 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng k2 is set
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
k1 .. (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D + (k1 .. (k2 /^ D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 .. k2) - D is ext-real V14() V32() V33() set
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k2) - D is ext-real V14() V32() V33() Element of REAL
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k2 /^ D) is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
D + k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
D + i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom k2 is Element of bool NAT
k2 . (D + k2) is set
(k2 /^ D) . k2 is set
k2 . (D + i) is set
(k2 /^ D) . i is set
i + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 . (i + D) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
<*> f is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined f -valued Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of f
(<*> f) /^ D is Relation-like NAT -defined f -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of f
len (<*> f) is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
D + f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 is non empty set
k2 is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
k2 /^ (D + f) is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
k2 /^ D is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
(k2 /^ D) /^ f is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k2) - D is ext-real V14() V32() V33() Element of REAL
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom ((k2 /^ D) /^ f) is Element of bool NAT
i + f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
dom (k2 /^ D) is Element of bool NAT
((k2 /^ D) /^ f) . i is set
(k2 /^ D) . (i + f) is set
(i + f) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k2 . ((i + f) + D) is set
i + (D + f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k2 . (i + (D + f)) is set
len ((k2 /^ D) /^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (k2 /^ D)) - f is ext-real V14() V32() V33() Element of REAL
(len k2) - (D + f) is ext-real V14() V32() V33() Element of REAL
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k2) - D is ext-real V14() V32() V33() Element of REAL
(len (k2 /^ D)) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*> k1 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined k1 -valued Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of k1
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*> k1 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined k1 -valued Function-like one-to-one constant functional V32() V33() V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of k1
(<*> k1) /^ f is Relation-like NAT -defined k1 -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of k1
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is non empty set
k1 is Element of f
k2 is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
rng k2 is set
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ D is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
(k2 /^ D) :- k1 is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
k2 :- k1 is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
<*k1*> is non empty trivial Relation-like NAT -defined f -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of f
k1 .. (k2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 /^ D) /^ (k1 .. (k2 /^ D)) is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
<*k1*> ^ ((k2 /^ D) /^ (k1 .. (k2 /^ D))) is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
D + (k1 .. (k2 /^ D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ (D + (k1 .. (k2 /^ D))) is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
<*k1*> ^ (k2 /^ (D + (k1 .. (k2 /^ D)))) is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
k2 /^ (k1 .. k2) is Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
<*k1*> ^ (k2 /^ (k1 .. k2)) is non empty Relation-like NAT -defined f -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of f
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 /^ 1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
D + f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 is non empty set
k2 is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ f is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
Rev (k2 /^ f) is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
Rev k2 is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
(Rev k2) | D is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
len (Rev k2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len ((Rev k2) | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k2) - f is ext-real V14() V32() V33() Element of REAL
len (k2 /^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom ((Rev k2) | D) is Element of bool NAT
dom (Rev k2) is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(len (k2 /^ f)) - i is ext-real V14() V32() V33() Element of REAL
(len (k2 /^ f)) - 1 is ext-real V14() V32() V33() Element of REAL
((len (k2 /^ f)) - i) + 1 is ext-real V14() V32() V33() Element of REAL
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k2 /^ f) is Element of bool NAT
((Rev k2) | D) . i is set
((Rev k2) | D) /. i is Element of k1
(Rev k2) /. i is Element of k1
(Rev k2) . i is set
(len (k2 /^ f)) + f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len (k2 /^ f)) + f) - i is ext-real V14() V32() V33() Element of REAL
(((len (k2 /^ f)) + f) - i) + 1 is ext-real V14() V32() V33() Element of REAL
k2 . ((((len (k2 /^ f)) + f) - i) + 1) is set
(k2 + 1) + f is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 . ((k2 + 1) + f) is set
(k2 /^ f) . (((len (k2 /^ f)) - i) + 1) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
D + f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 is non empty set
k2 is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 | f is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
Rev (k2 | f) is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
Rev k2 is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
(Rev k2) /^ D is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
len (Rev k2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Rev (Rev k2) is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
(Rev (Rev k2)) | f is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
Rev ((Rev (Rev k2)) | f) is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
Rev ((Rev k2) /^ D) is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
Rev (Rev ((Rev k2) /^ D)) is Relation-like NAT -defined k1 -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of k1
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (k1 |-- f) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev k1) -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng k1 is set
rng (Rev k1) is set
f .. (Rev k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f .. (Rev k1)) - 1 is ext-real V14() V32() V33() Element of REAL
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f .. k1) + (f .. (Rev k1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + (f .. k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (k1 /^ (f .. k1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev k1) | k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg k2 is V34() k2 -element Element of bool NAT
(Rev k1) | (Seg k2) is Relation-like NAT -defined Seg k2 -defined NAT -defined Seg k2 -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,D:]
[:NAT,D:] is Relation-like V34() set
bool [:NAT,D:] is V34() set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (k1 :- f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev k1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
rng (Rev k1) is set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
k1 |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (k1 |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (<*f*> ^ (k1 |-- f)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (k1 |-- f) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev (k1 |-- f)) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev k1) -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((Rev k1) -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (k1 -: f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev k1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
rng (Rev k1) is set
k1 -| f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k1 -| f) ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev ((k1 -| f) ^ <*f*>) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev (k1 -| f) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ (Rev (k1 -| f)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(Rev k1) |-- f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*f*> ^ ((Rev k1) |-- f) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
D is non empty set
k1 is Element of D
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng f is set
f :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f -: k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f :- k1) ^ ((f -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 is Element of D
(D,f,k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng f is non empty set
f :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f -: k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f :- k1) ^ ((f -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng f is non empty set
rng f is non empty set
D is non empty set
the Element of D is Element of D
<* the Element of D*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<* the Element of D*> /. 1 is Element of D
len <* the Element of D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<* the Element of D*> /. (len <* the Element of D*>) is Element of D
the Element of D is Element of D
<* the Element of D, the Element of D*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
len <* the Element of D, the Element of D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<* the Element of D, the Element of D*> /. (len <* the Element of D, the Element of D*>) is Element of D
<* the Element of D, the Element of D*> /. 1 is Element of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. 1 is Element of D
(D,f,(f /. 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
len <*(f /. 1)*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng f is set
f :- (f /. 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f -: (f /. 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f -: (f /. 1)) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f :- (f /. 1)) ^ ((f -: (f /. 1)) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f ^ ((f -: (f /. 1)) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. 1)*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f ^ (<*(f /. 1)*> /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f ^ {} is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like (D) FinSequence of D
f is Element of D
(D,k1,f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is non empty set
rng k1 is non empty set
k1 /. 1 is Element of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k1 -: f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len ((k1 -: f) /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (k1 -: f)) - 1 is ext-real V14() V32() V33() Element of REAL
(len ((k1 -: f) /^ 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom ((k1 -: f) /^ 1) is Element of bool NAT
dom (k1 :- f) is non empty Element of bool NAT
(D,k1,f) /. 1 is Element of D
(k1 :- f) /. 1 is Element of D
(k1 -: f) /. (f .. k1) is Element of D
(k1 -: f) /. ((len ((k1 -: f) /^ 1)) + 1) is Element of D
((k1 -: f) /^ 1) /. (len ((k1 -: f) /^ 1)) is Element of D
len (k1 :- f) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (k1 :- f)) + (len ((k1 -: f) /^ 1)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((k1 :- f) ^ ((k1 -: f) /^ 1)) /. ((len (k1 :- f)) + (len ((k1 -: f) /^ 1))) is Element of D
len (D,k1,f) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,k1,f) /. (len (D,k1,f)) is Element of D
rng k1 is non empty set
k1 /. 1 is Element of D
rng k1 is non empty set
k1 /. 1 is Element of D
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
(D,k1,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,k1,f) is set
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng ((k1 -: f) /^ 1) is set
rng (k1 -: f) is set
rng ((k1 :- f) ^ ((k1 -: f) /^ 1)) is non empty set
rng (k1 :- f) is non empty set
(rng (k1 :- f)) \/ (rng ((k1 -: f) /^ 1)) is non empty set
k2 is set
dom k1 is Element of bool NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 . i is set
k1 /. i is Element of D
len (k1 :- f) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ (k1 /^ (f .. k1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (<*f*> ^ (k1 /^ (f .. k1))) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len <*f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k1 /^ (f .. k1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*f*>) + (len (k1 /^ (f .. k1))) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 + (len (k1 /^ (f .. k1))) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k1 :- f) is non empty Element of bool NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /. (len k1) is Element of D
(k1 :- f) /. (len (k1 :- f)) is Element of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (f .. k1) is V34() f .. k1 -element Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k1 -: f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len ((k1 -: f) /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (k1 -: f)) - 1 is ext-real V14() V32() V33() Element of REAL
(len ((k1 -: f) /^ 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom ((k1 -: f) /^ 1) is Element of bool NAT
(k1 -: f) /. 1 is Element of D
<*((k1 -: f) /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
len <*((k1 -: f) /. 1)*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
<*((k1 -: f) /. 1)*> ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k1 -: f) /^ 1) /. k2 is Element of D
(k1 -: f) /. i is Element of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i - (f .. k1) is ext-real V14() V32() V33() set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k1) - (f .. k1) is ext-real V14() V32() V33() Element of REAL
len (k1 :- f) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len k1) - (f .. k1)) + 1 is ext-real V14() V32() V33() Element of REAL
dom (k1 :- f) is non empty Element of bool NAT
k2 + (f .. k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 :- f) /. (k2 + 1) is Element of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
(D,k1,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,k1,f) is set
{f} is non empty trivial 1 -element set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
rng <*f*> is non empty trivial 1 -element set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 /^ (f .. k1)) is set
(rng <*f*>) \/ (rng (k1 /^ (f .. k1))) is non empty set
<*f*> ^ (k1 /^ (f .. k1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (<*f*> ^ (k1 /^ (f .. k1))) is non empty set
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 :- f) is non empty set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng ((k1 -: f) /^ 1) is set
(rng (k1 :- f)) \/ (rng ((k1 -: f) /^ 1)) is non empty set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
(D,k1,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k1,f) /. 1 is Element of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /^ (f .. k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ (k1 /^ (f .. k1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ (k1 /^ (f .. k1))) ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 /^ (f .. k1)) ^ ((k1 -: f) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ ((k1 /^ (f .. k1)) ^ ((k1 -: f) /^ 1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k1,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,k1,f),f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k1 is set
(D,k1,f) /. 1 is Element of D
k2 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k2,f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k2,f) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,k1,f) is set
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
len <*f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,k2,f) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k1,f) ^ (<*f*> /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k1,f) ^ {} is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng k1 is set
rng k1 is set
D is non empty set
f is Element of D
<*f*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,<*f*>,f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> /. 1 is Element of D
D is non empty set
f is Element of D
k1 is Element of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,<*f,k1*>,f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> /. 1 is Element of D
D is non empty set
f is Element of D
k1 is Element of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,<*f,k1*>,k1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
rng <*f,k1*> is non empty set
{f,k1} is non empty set
<*f,k1*> :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f,k1*> -: k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f,k1*> :- k1) ^ ((<*f,k1*> -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> ^ ((<*f,k1*> -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> ^ (<*f,k1*> /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> ^ <*k1*> is non empty Relation-like NAT -defined D -valued Function-like V34() 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Element of D
k2 is Element of D
<*f,k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,<*f,k1,k2*>,f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1,k2*> /. 1 is Element of D
D is non empty set
f is Element of D
k1 is Element of D
k2 is Element of D
<*f,k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,<*f,k1,k2*>,k1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k2,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
rng <*f,k1,k2*> is non empty set
{f,k1,k2} is set
<*f,k1,k2*> :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1,k2*> -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f,k1,k2*> -: k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f,k1,k2*> :- k1) ^ ((<*f,k1,k2*> -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k2*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k2*> ^ ((<*f,k1,k2*> -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k2*> ^ (<*f,k1*> /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*k1,k2*> ^ <*k1*> is non empty Relation-like NAT -defined D -valued Function-like V34() 2 + 1 -element FinSequence-like FinSubsequence-like FinSequence of D
2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Element of D
k1 is Element of D
<*k1,f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
k2 is Element of D
<*k2,f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 3 -element FinSequence-like FinSubsequence-like FinSequence of D
(D,<*k2,f,k1*>,k1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*k2,f,k1*> is non empty set
{k2,f,k1} is set
<*k2,f,k1*> :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k2,f,k1*> -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*k2,f,k1*> -: k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*k2,f,k1*> :- k1) ^ ((<*k2,f,k1*> -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> ^ ((<*k2,f,k1*> -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k2,f,k1*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> ^ (<*k2,f,k1*> /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k1*> is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() 2 -element FinSequence-like FinSubsequence-like FinSequence of D
<*k1*> ^ <*f,k1*> is non empty Relation-like NAT -defined D -valued Function-like V34() 1 + 2 -element FinSequence-like FinSubsequence-like FinSequence of D
1 + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is non empty non trivial Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like (D) FinSequence of D
f /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (f /^ 1) is set
rng f is non empty set
k1 is set
f /. 1 is Element of D
<*(f /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. 1)*> ^ (f /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*(f /. 1)*> is non empty trivial 1 -element set
(rng <*(f /. 1)*>) \/ (rng (f /^ 1)) is non empty set
{(f /. 1)} is non empty trivial 1 -element set
len f is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /. (len f) is Element of D
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (f /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) - 1 is ext-real V14() V32() V33() Element of REAL
dom (f /^ 1) is Element of bool NAT
(len (f /^ 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f /^ 1) /. (len (f /^ 1)) is Element of D
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 /^ 1) is set
(D,k1,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,k1,f) is set
rng k1 is set
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k1 :- f) is non empty set
rng ((k1 -: f) /^ 1) is set
(rng (k1 :- f)) \/ (rng ((k1 -: f) /^ 1)) is non empty set
k2 is set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f .. (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 .. (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f .. (k1 /^ 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 .. (k1 /^ 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k1 /^ 1) is Element of bool NAT
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len k1) - 1 is ext-real V14() V32() V33() Element of REAL
len (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (k1 /^ 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i is Element of D
i .. (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 /^ 1) /. (i .. (k1 /^ 1)) is Element of D
(i .. (k1 /^ 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /. ((i .. (k1 /^ 1)) + 1) is Element of D
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 .. (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f .. (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 /^ 1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng ((k1 /^ 1) -: f) is set
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 .. k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f .. (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 .. (k1 /^ 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng k1 is set
rng k1 is set
D is non empty set
f is Element of D
k1 is Element of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
k2 -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: k1) is set
(rng k2) \ (rng (k2 -: k1)) is Element of bool (rng k2)
bool (rng k2) is set
(D,k2,k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,k2,k1),f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k2,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 -: k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- k1) ^ ((k2 -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 .. (k2 :- k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng ((k2 -: k1) /^ 1) is set
k2 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 /^ 1) is set
rng (D,k2,k1) is set
k1 .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng (k2 :- k1) is non empty set
(rng (k2 -: k1)) \/ (rng (k2 :- k1)) is non empty set
f .. (k2 :- k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 :- k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng ((k2 :- k1) /^ 1) is set
(rng ((k2 :- k1) /^ 1)) \ (rng ((k2 -: k1) /^ 1)) is Element of bool (rng ((k2 :- k1) /^ 1))
bool (rng ((k2 :- k1) /^ 1)) is set
f .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((k2 :- k1) ^ ((k2 -: k1) /^ 1)) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 :- k1) ^ ((k2 -: k1) /^ 1)) :- f) ^ ((((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- k1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- k1) :- f) ^ ((k2 -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 :- k1) :- f) ^ ((k2 -: k1) /^ 1)) ^ ((((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ ((k2 -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- f) ^ ((k2 -: k1) /^ 1)) ^ ((((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- k1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- k1) -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- f) ^ ((k2 -: k1) /^ 1)) ^ (((k2 :- k1) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- k1) /^ 1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- f) ^ ((k2 -: k1) /^ 1)) ^ (((k2 :- k1) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) /^ 1) ^ (((k2 :- k1) /^ 1) -: f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ (((k2 -: k1) /^ 1) ^ (((k2 :- k1) /^ 1) -: f)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) /^ 1) ^ ((k2 :- k1) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) /^ 1) ^ ((k2 :- k1) /^ 1)) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ ((((k2 -: k1) /^ 1) ^ ((k2 :- k1) /^ 1)) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 -: k1) ^ ((k2 :- k1) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) ^ ((k2 :- k1) /^ 1)) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) ^ ((k2 :- k1) /^ 1)) /^ 1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ ((((k2 -: k1) ^ ((k2 :- k1) /^ 1)) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 /^ 1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ ((k2 /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ ((k2 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Element of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
rng k2 is set
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 :- k1) is non empty set
(rng k2) \ (rng (k2 :- k1)) is Element of bool (rng k2)
bool (rng k2) is set
(D,k2,k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,k2,k1),f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k2,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: k1) is set
(rng (k2 -: k1)) \/ (rng (k2 :- k1)) is non empty set
(k2 :- k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 -: k1) ^ ((k2 :- k1) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f .. (k2 -: k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -: k1) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng ((k2 -: k1) /^ 1) is set
(rng ((k2 -: k1) /^ 1)) \ (rng (k2 :- k1)) is Element of bool (rng ((k2 -: k1) /^ 1))
bool (rng ((k2 -: k1) /^ 1)) is set
(k2 :- k1) ^ ((k2 -: k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,k2,k1) is set
(rng (k2 :- k1)) \/ (rng ((k2 -: k1) /^ 1)) is non empty set
((k2 :- k1) ^ ((k2 -: k1) /^ 1)) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 :- k1) ^ ((k2 -: k1) /^ 1)) :- f) ^ ((((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) /^ 1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) /^ 1) :- f) ^ ((((k2 :- k1) ^ ((k2 -: k1) /^ 1)) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) /^ 1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- k1) ^ (((k2 -: k1) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- k1) ^ (((k2 -: k1) /^ 1) -: f)) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) /^ 1) :- f) ^ (((k2 :- k1) ^ (((k2 -: k1) /^ 1) -: f)) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 :- k1) /^ 1) ^ (((k2 -: k1) /^ 1) -: f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) /^ 1) :- f) ^ (((k2 :- k1) /^ 1) ^ (((k2 -: k1) /^ 1) -: f)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) /^ 1) :- f) ^ ((k2 :- k1) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((k2 -: k1) /^ 1) :- f) ^ ((k2 :- k1) /^ 1)) ^ (((k2 -: k1) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) /^ 1) ^ ((k2 :- k1) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) /^ 1) ^ ((k2 :- k1) /^ 1)) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((k2 -: k1) /^ 1) ^ ((k2 :- k1) /^ 1)) :- f) ^ (((k2 -: k1) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) ^ ((k2 :- k1) /^ 1)) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((k2 -: k1) ^ ((k2 :- k1) /^ 1)) /^ 1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((k2 -: k1) ^ ((k2 :- k1) /^ 1)) /^ 1) :- f) ^ (((k2 -: k1) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 /^ 1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 /^ 1) :- f) ^ (((k2 -: k1) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ (((k2 -: k1) /^ 1) -: f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 -: k1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((k2 -: k1) -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ (((k2 -: k1) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 :- f) ^ ((k2 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
k1 is Element of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 /^ 1) is set
(D,k2,k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,k2,k1),f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k2,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
k2 -| k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*k1*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k2 -| k1) ^ <*k1*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 |-- k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((k2 -| k1) ^ <*k1*>) ^ (k2 |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng ((k2 -| k1) ^ <*k1*>) is non empty set
rng (k2 |-- k1) is set
(rng ((k2 -| k1) ^ <*k1*>)) \+\ (rng (k2 |-- k1)) is set
(rng ((k2 -| k1) ^ <*k1*>)) \ (rng (k2 |-- k1)) is set
(rng (k2 |-- k1)) \ (rng ((k2 -| k1) ^ <*k1*>)) is set
((rng ((k2 -| k1) ^ <*k1*>)) \ (rng (k2 |-- k1))) \/ ((rng (k2 |-- k1)) \ (rng ((k2 -| k1) ^ <*k1*>))) is set
rng <*k1*> is non empty trivial 1 -element set
(rng (k2 |-- k1)) \/ (rng <*k1*>) is non empty set
<*k1*> ^ (k2 |-- k1) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (<*k1*> ^ (k2 |-- k1)) is non empty set
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 :- k1) is non empty set
rng <*k1*> is non empty trivial 1 -element set
{k1} is non empty trivial 1 -element set
rng <*k1*> is non empty trivial 1 -element set
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 :- k1) is non empty set
rng <*k1*> is non empty trivial 1 -element set
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 :- k1) is non empty set
k2 -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: k1) is set
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 :- k1) is non empty set
k2 -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: k1) is set
k2 :- k1 is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 :- k1) is non empty set
k2 -: k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (k2 -: k1) is set
k2 /. 1 is Element of D
<*(k2 /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*(k2 /. 1)*> ^ (k2 /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*(k2 /. 1)*> is non empty trivial 1 -element set
(rng <*(k2 /. 1)*>) \+\ (rng (k2 /^ 1)) is set
(rng <*(k2 /. 1)*>) \ (rng (k2 /^ 1)) is set
(rng (k2 /^ 1)) \ (rng <*(k2 /. 1)*>) is set
((rng <*(k2 /. 1)*>) \ (rng (k2 /^ 1))) \/ ((rng (k2 /^ 1)) \ (rng <*(k2 /. 1)*>)) is set
{(k2 /. 1)} is non empty trivial 1 -element set
f .. k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(rng k2) \ (rng (k2 -: k1)) is Element of bool (rng k2)
bool (rng k2) is set
(rng k2) \ (rng (k2 :- k1)) is Element of bool (rng k2)
bool (rng k2) is set
(rng k2) \ (rng (k2 -: k1)) is Element of bool (rng k2)
bool (rng k2) is set
(rng k2) \ (rng (k2 :- k1)) is Element of bool (rng k2)
rng k2 is set
rng k2 is set
D is non empty set
f is Element of D
k1 is Element of D
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k2,k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,k2,k1),f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k2,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng k2 is set
k2 /. 1 is Element of D
<*(k2 /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
k2 /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(k2 /. 1)*> ^ (k2 /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng <*(k2 /. 1)*> is non empty trivial 1 -element set
rng (k2 /^ 1) is set
(rng <*(k2 /. 1)*>) \/ (rng (k2 /^ 1)) is non empty set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
{(k2 /. 1)} is non empty trivial 1 -element set
k2 /. (len k2) is Element of D
dom k2 is Element of bool NAT
rng k2 is set
rng k2 is set
D is non empty set
f is Element of D
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,k1,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (D,k1,f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(Rev k1),f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (k1 :- f) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (k1 :- f)) - 1 is ext-real V14() V32() V33() Element of REAL
k1 /. 1 is Element of D
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 /. (len k1) is Element of D
rng k1 is set
k1 -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /. 1 is Element of D
<*((k1 -: f) /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
(k1 -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*((k1 -: f) /. 1)*> ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(k1 /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*(k1 /. 1)*> ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 :- f) | k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k1 :- f) /. (len (k1 :- f)) is Element of D
<*((k1 :- f) /. (len (k1 :- f)))*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
((k1 :- f) | k2) ^ <*((k1 :- f) /. (len (k1 :- f)))*> is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(k1 /. (len k1))*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
((k1 :- f) | k2) ^ <*(k1 /. (len k1))*> is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (Rev k1) is set
(k1 :- f) ^ ((k1 -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((k1 :- f) ^ ((k1 -: f) /^ 1)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((k1 -: f) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (k1 :- f) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev ((k1 -: f) /^ 1)) ^ (Rev (k1 :- f)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((k1 :- f) | k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(k1 /. (len k1))*> ^ (Rev ((k1 :- f) | k2)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev ((k1 -: f) /^ 1)) ^ (<*(k1 /. (len k1))*> ^ (Rev ((k1 :- f) | k2))) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev ((k1 -: f) /^ 1)) ^ <*(k1 /. 1)*> is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev ((k1 -: f) /^ 1)) ^ <*(k1 /. 1)*>) ^ (Rev ((k1 :- f) | k2)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (k1 -: f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev (k1 -: f)) ^ (Rev ((k1 :- f) | k2)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev (k1 :- f)) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev (k1 -: f)) ^ ((Rev (k1 :- f)) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev k1) -: f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev k1) -: f) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev (k1 -: f)) ^ (((Rev k1) -: f) /^ 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev k1) :- f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev k1) :- f) ^ (((Rev k1) -: f) /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is trivial Relation-like NAT -defined D -valued Function-like constant V34() FinSequence-like FinSubsequence-like FinSequence of D
rng f is trivial set
k1 is set
{k1} is non empty trivial 1 -element set
dom f is trivial Element of bool NAT
k2 is set
i is set
[k2,i] is non empty set
{k2,i} is non empty set
{k2} is non empty trivial 1 -element set
{{k2,i},{k2}} is non empty set
<*i*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*i*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + (len k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f ^ k1 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len (f ^ k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f ^ k1) . D is set
D - (len f) is ext-real V14() V32() V33() Element of REAL
k1 . (D - (len f)) is set
((len f) + (len k1)) - (len f) is ext-real V14() V32() V33() Element of REAL
(len f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) + 1) - (len f) is ext-real V14() V32() V33() Element of REAL
D -' (len f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + (D -' (len f)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) + (D - (len f)) is ext-real V14() V32() V33() Element of REAL
dom k1 is Element of bool NAT
D is non empty set
f is set
<*f*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 ^ <*f*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k1 ^ <*f*>) . 1 is set
k1 . 1 is set
k1 /. 1 is Element of D
<*f*> ^ k1 is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(len k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(<*f*> ^ k1) . ((len k1) + 1) is set
k1 . (len k1) is set
k1 /. (len k1) is Element of D
dom k1 is Element of bool NAT
len <*f*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len <*f*>) + (len k1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(<*f*> ^ k1) . ((len <*f*>) + (len k1)) is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Rev D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D . 1 is set
<*(D . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
D is non empty set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ k1) | (k2 -' k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | k2) /^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 -' f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D /^ (f -' 1) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D /^ (f -' 1)) | ((k1 -' f) + 1) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D /^ (k1 -' 1) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D /^ (k1 -' 1)) | ((f -' k1) + 1) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Rev ((D /^ (k1 -' 1)) | ((f -' k1) + 1)) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(f,k1,k2) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -' k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' k2) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k2 -' 1)) | ((k1 -' k2) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Rev f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (D,f,k1,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(len f) -' k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' k2) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,(Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) -' (k1 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) - (k1 -' 1) is ext-real V14() V32() V33() Element of REAL
k1 - 1 is ext-real V14() V32() V33() Element of REAL
(len f) - (k1 - 1) is ext-real V14() V32() V33() Element of REAL
(len f) - k1 is ext-real V14() V32() V33() Element of REAL
((len f) - k1) + 1 is ext-real V14() V32() V33() Element of REAL
(len f) - k2 is ext-real V14() V32() V33() Element of REAL
k2 - k1 is ext-real V14() V32() V33() set
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' (k1 -' 1)) -' ((k2 -' k1) + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((len f) -' k1) + 1) - ((k2 -' k1) + 1) is ext-real V14() V32() V33() Element of REAL
(k2 - k1) + 1 is ext-real V14() V32() V33() Element of REAL
(((len f) - k1) + 1) - ((k2 - k1) + 1) is ext-real V14() V32() V33() Element of REAL
(len f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) + 1) - 1 is ext-real V14() V32() V33() Element of REAL
(((len f) + 1) - 1) - k2 is ext-real V14() V32() V33() Element of REAL
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (k1 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) + ((k2 -' k1) + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' k2) + ((k2 -' k1) + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) - k2) + ((k2 - k1) + 1) is ext-real V14() V32() V33() Element of REAL
((len f) -' (k1 -' 1)) -' ((len f) -' k2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((len f) -' k1) + 1) - ((len f) -' k2) is ext-real V14() V32() V33() Element of REAL
(((len f) - k1) + 1) - ((len f) - k2) is ext-real V14() V32() V33() Element of REAL
((len f) -' (k1 -' 1)) + (k1 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) - (k1 -' 1)) + (k1 -' 1) is ext-real V14() V32() V33() Element of REAL
(((len f) -' k1) + 1) -' (((len f) -' k2) + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((((len f) -' k1) + 1) -' (((len f) -' k2) + 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((len f) -' k1) + 1) - (((len f) -' k2) + 1) is ext-real V14() V32() V33() Element of REAL
((((len f) -' k1) + 1) - (((len f) -' k2) + 1)) + 1 is ext-real V14() V32() V33() Element of REAL
((len f) - k2) + 1 is ext-real V14() V32() V33() Element of REAL
(((len f) - k1) + 1) - (((len f) - k2) + 1) is ext-real V14() V32() V33() Element of REAL
((((len f) - k1) + 1) - (((len f) - k2) + 1)) + 1 is ext-real V14() V32() V33() Element of REAL
(((len f) -' k2) + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(Rev f) /^ ((((len f) -' k2) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) /^ ((((len f) -' k2) + 1) -' 1)) | ((k2 -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev f) /^ ((len f) -' k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) /^ ((len f) -' k2)) | (((len f) -' (k1 -' 1)) -' ((len f) -' k2)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev f) | ((len f) -' (k1 -' 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len f) -' k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (f /^ (k1 -' 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev (f /^ (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) -' (k2 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) - (k2 -' 1) is ext-real V14() V32() V33() Element of REAL
k2 - 1 is ext-real V14() V32() V33() Element of REAL
(len f) - (k2 - 1) is ext-real V14() V32() V33() Element of REAL
(len f) - k2 is ext-real V14() V32() V33() Element of REAL
((len f) - k2) + 1 is ext-real V14() V32() V33() Element of REAL
(((len f) -' k2) + 1) -' (((len f) -' k1) + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((((len f) -' k2) + 1) -' (((len f) -' k1) + 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((len f) -' k2) + 1) - (((len f) -' k1) + 1) is ext-real V14() V32() V33() Element of REAL
((((len f) -' k2) + 1) - (((len f) -' k1) + 1)) + 1 is ext-real V14() V32() V33() Element of REAL
(len f) - k1 is ext-real V14() V32() V33() Element of REAL
((len f) - k1) + 1 is ext-real V14() V32() V33() Element of REAL
(((len f) - k2) + 1) - (((len f) - k1) + 1) is ext-real V14() V32() V33() Element of REAL
((((len f) - k2) + 1) - (((len f) - k1) + 1)) + 1 is ext-real V14() V32() V33() Element of REAL
k1 - k2 is ext-real V14() V32() V33() set
(k1 - k2) + 1 is ext-real V14() V32() V33() Element of REAL
k1 -' k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' k2) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' (k2 -' 1)) -' ((len f) -' k1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((len f) -' k2) + 1) - ((len f) -' k1) is ext-real V14() V32() V33() Element of REAL
(((len f) - k2) + 1) - ((len f) - k1) is ext-real V14() V32() V33() Element of REAL
((len f) -' (k2 -' 1)) + (k2 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) - (k2 -' 1)) + (k2 -' 1) is ext-real V14() V32() V33() Element of REAL
((len f) -' (k2 -' 1)) -' ((k1 -' k2) + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((len f) -' k2) + 1) - ((k1 -' k2) + 1) is ext-real V14() V32() V33() Element of REAL
(((len f) - k2) + 1) - ((k1 - k2) + 1) is ext-real V14() V32() V33() Element of REAL
(len f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) + 1) - 1 is ext-real V14() V32() V33() Element of REAL
(((len f) + 1) - 1) - k1 is ext-real V14() V32() V33() Element of REAL
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (k2 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)) + ((k1 -' k2) + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' k1) + ((k1 -' k2) + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) - k1) + ((k1 - k2) + 1) is ext-real V14() V32() V33() Element of REAL
(((len f) -' k1) + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(Rev f) /^ ((((len f) -' k1) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) /^ ((((len f) -' k1) + 1) -' 1)) | ((k1 -' k2) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (((Rev f) /^ ((((len f) -' k1) + 1) -' 1)) | ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev f) /^ ((len f) -' k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) /^ ((len f) -' k1)) | (((len f) -' (k2 -' 1)) -' ((len f) -' k1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (((Rev f) /^ ((len f) -' k1)) | (((len f) -' (k2 -' 1)) -' ((len f) -' k1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev f) | ((len f) -' (k2 -' 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len f) -' k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len f) -' k1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (f /^ (k2 -' 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev (f /^ (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((Rev (f /^ (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k2 -' 1)) | ((k1 -' k2) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 + f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 /^ f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 /^ f) . k1 is set
k2 . (k1 + f) is set
(k1 + f) - f is ext-real V14() V32() V33() Element of REAL
(len k2) - f is ext-real V14() V32() V33() Element of REAL
f + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
len (k2 /^ f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom (k2 /^ f) is Element of bool NAT
D is non empty set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Rev k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev k1) . f is set
(len k1) - f is ext-real V14() V32() V33() Element of REAL
((len k1) - f) + 1 is ext-real V14() V32() V33() Element of REAL
k1 . (((len k1) - f) + 1) is set
dom k1 is Element of bool NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(D,f,1,k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f /^ (1 -' 1)) | ((k1 -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,(len f)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(len f) -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f /^ (k1 -' 1)) | (((len f) -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (k1 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) - (k1 -' 1) is ext-real V14() V32() V33() Element of REAL
(len f) - k1 is ext-real V14() V32() V33() Element of REAL
((len f) - k1) + 1 is ext-real V14() V32() V33() Element of REAL
k1 - 1 is ext-real V14() V32() V33() Element of REAL
(len f) - (k1 - 1) is ext-real V14() V32() V33() Element of REAL
0 - 1 is ext-real non positive negative non empty V14() V32() V33() Element of REAL
(len f) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (len f) is V34() len f -element Element of bool NAT
Seg (((len f) -' k1) + 1) is non empty V34() ((len f) -' k1) + 1 -element Element of bool NAT
dom (f /^ (k1 -' 1)) is Element of bool NAT
(f /^ (k1 -' 1)) | (Seg (((len f) -' k1) + 1)) is Relation-like NAT -defined Seg (((len f) -' k1) + 1) -defined NAT -defined Seg (((len f) -' k1) + 1) -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,D:]
[:NAT,D:] is Relation-like V34() set
bool [:NAT,D:] is V34() set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (len (f /^ (k1 -' 1))) is V34() len (f /^ (k1 -' 1)) -element Element of bool NAT
(f /^ (k1 -' 1)) | (Seg (len (f /^ (k1 -' 1)))) is Relation-like NAT -defined Seg (len (f /^ (k1 -' 1))) -defined NAT -defined Seg (len (f /^ (k1 -' 1))) -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,D:]
[:NAT,D:] is Relation-like V34() set
bool [:NAT,D:] is V34() set
dom (f /^ (k1 -' 1)) is Element of bool NAT
(f /^ (k1 -' 1)) | (dom (f /^ (k1 -' 1))) is Relation-like NAT -defined dom (f /^ (k1 -' 1)) -defined NAT -defined D -valued Function-like FinSubsequence-like Element of bool [:NAT,D:]
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k1,k2) . 1 is set
f . k1 is set
len (D,f,k1,k2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 -' k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' k2) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (k2 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) - (k2 -' 1) is ext-real V14() V32() V33() Element of REAL
k2 - 1 is ext-real V14() V32() V33() Element of REAL
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,i,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,k2) . 1 is set
k2 -' i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' i) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (i -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (i -' 1)) | ((k2 -' i) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (i -' 1)) | ((k2 -' i) + 1)) . 1 is set
Seg ((k2 -' i) + 1) is non empty V34() (k2 -' i) + 1 -element Element of bool NAT
(f /^ (i -' 1)) | (Seg ((k2 -' i) + 1)) is Relation-like NAT -defined Seg ((k2 -' i) + 1) -defined NAT -defined Seg ((k2 -' i) + 1) -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,D:]
[:NAT,D:] is Relation-like V34() set
bool [:NAT,D:] is V34() set
((f /^ (i -' 1)) | (Seg ((k2 -' i) + 1))) . 1 is set
i - 1 is ext-real V14() V32() V33() Element of REAL
1 + (i -' 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 + (i - 1) is ext-real V14() V32() V33() Element of REAL
(len f) - (i -' 1) is ext-real V14() V32() V33() Element of REAL
((len f) - (i -' 1)) + (i -' 1) is ext-real V14() V32() V33() Element of REAL
len (f /^ (i -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (len (f /^ (i -' 1))) is V34() len (f /^ (i -' 1)) -element Element of bool NAT
dom (f /^ (i -' 1)) is Element of bool NAT
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(dom (f /^ (i -' 1))) /\ (Seg ((k2 -' i) + 1)) is Element of bool NAT
dom ((f /^ (i -' 1)) | (Seg ((k2 -' i) + 1))) is Element of bool NAT
(f /^ (i -' 1)) . 1 is set
f . i is set
k1 - k2 is ext-real V14() V32() V33() set
(k2 -' 1) + ((k1 -' k2) + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 - (k2 - 1) is ext-real V14() V32() V33() Element of REAL
(k2 - 1) + (k1 - (k2 - 1)) is ext-real V14() V32() V33() Element of REAL
(k1 - k2) + 1 is ext-real V14() V32() V33() Element of REAL
k1 - (k2 -' 1) is ext-real V14() V32() V33() set
(f /^ (k2 -' 1)) | ((k1 -' k2) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
dom ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is Element of bool NAT
dom (f /^ (k2 -' 1)) is Element of bool NAT
((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) . (len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) is set
((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) /. ((k1 -' k2) + 1) is Element of D
(f /^ (k2 -' 1)) /. ((k1 -' k2) + 1) is Element of D
f /. ((k2 -' 1) + ((k1 -' k2) + 1)) is Element of D
Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) . 1 is set
(len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) - 1 is ext-real V14() V32() V33() Element of REAL
((len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) - 1) + 1 is ext-real V14() V32() V33() Element of REAL
((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) . (((len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) - 1) + 1) is set
k1 - 1 is ext-real V14() V32() V33() Element of REAL
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (k1 -' 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) - (k1 -' 1) is ext-real V14() V32() V33() Element of REAL
(f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 - k1 is ext-real V14() V32() V33() set
(k2 - k1) + 1 is ext-real V14() V32() V33() Element of REAL
k2 - (k1 - 1) is ext-real V14() V32() V33() Element of REAL
k2 - (k1 -' 1) is ext-real V14() V32() V33() set
len ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) . i is set
i + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(i + k1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f . ((i + k1) -' 1) is set
i + (k1 - 1) is ext-real V14() V32() V33() Element of REAL
(k2 - (k1 - 1)) + (k1 - 1) is ext-real V14() V32() V33() Element of REAL
i + (k1 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 + i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(i + k1) - 1 is ext-real V14() V32() V33() Element of REAL
((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) . i is set
(f /^ (k1 -' 1)) . i is set
f . (i + (k1 -' 1)) is set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) . i is set
i + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(i + k1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f . ((i + k1) -' 1) is set
k1 - k2 is ext-real V14() V32() V33() set
(f /^ (k2 -' 1)) | ((k1 -' k2) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 - k2) + 1 is ext-real V14() V32() V33() Element of REAL
k1 - (k2 - 1) is ext-real V14() V32() V33() Element of REAL
k1 - (k2 -' 1) is ext-real V14() V32() V33() set
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) . i is set
k1 -' i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' i) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f . ((k1 -' i) + 1) is set
i + (k2 - 1) is ext-real V14() V32() V33() Element of REAL
(k1 - (k2 - 1)) + (k2 - 1) is ext-real V14() V32() V33() Element of REAL
i -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((k1 -' k2) + 1) + (i -' 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i - 1 is ext-real V14() V32() V33() Element of REAL
((k1 -' k2) + 1) + (i - 1) is ext-real V14() V32() V33() Element of REAL
((k1 -' k2) + 1) - (i - 1) is ext-real V14() V32() V33() Element of REAL
(((k1 -' k2) + 1) + (i - 1)) - (i - 1) is ext-real V14() V32() V33() Element of REAL
((k1 -' k2) + 1) - i is ext-real V14() V32() V33() Element of REAL
(((k1 -' k2) + 1) - i) + 1 is ext-real V14() V32() V33() Element of REAL
((k1 -' k2) + 1) -' i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(((k1 -' k2) + 1) -' i) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i + (len f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i + (k2 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((((k1 -' k2) + 1) -' i) + 1) + (k2 -' 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((((k1 -' k2) + 1) - i) + 1) + (k2 -' 1) is ext-real V14() V32() V33() Element of REAL
(k1 - (k2 - 1)) - i is ext-real V14() V32() V33() Element of REAL
((k1 - (k2 - 1)) - i) + 1 is ext-real V14() V32() V33() Element of REAL
(((k1 - (k2 - 1)) - i) + 1) + (k2 - 1) is ext-real V14() V32() V33() Element of REAL
k1 - i is ext-real V14() V32() V33() set
(k1 - i) + 1 is ext-real V14() V32() V33() Element of REAL
1 + k1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(1 + k1) - i is ext-real V14() V32() V33() Element of REAL
(i + (len f)) - i is ext-real V14() V32() V33() Element of REAL
(len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) - i is ext-real V14() V32() V33() Element of REAL
((len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) - i) + 1 is ext-real V14() V32() V33() Element of REAL
((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) . (((len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) - i) + 1) is set
(len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) -' i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) -' i) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) . (((len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) -' i) + 1) is set
(f /^ (k2 -' 1)) . ((((k1 -' k2) + 1) -' i) + 1) is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng f is set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,f,k1,k2) is set
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (f /^ (k1 -' 1)) is set
k1 -' k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' k2) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k2 -' 1)) | ((k1 -' k2) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is set
rng (f /^ (k2 -' 1)) is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,1,(len f)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(len f) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (1 -' 1)) | (((len f) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ 0 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 0) | (((len f) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | (((len f) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | (len f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,(len f),1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(len f) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len f) -' 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (1 -' 1)) | (((len f) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((f /^ (1 -' 1)) | (((len f) -' 1) + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ 0 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 0) | (len f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev ((f /^ 0) | (len f)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | (len f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Rev (f | (len f)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(1 -' 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (1 -' 1)) | ((1 -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
i is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 - k1 is ext-real V14() V32() V33() set
(k2 - k1) + 1 is ext-real V14() V32() V33() Element of REAL
k2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 + 1) - k1 is ext-real V14() V32() V33() Element of REAL
(D,f,k1,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k1,k2) . i is set
i + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(i + k1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f . ((i + k1) -' 1) is set
i -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(i -' 1) + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f . ((i -' 1) + k1) is set
(i + k1) - 1 is ext-real V14() V32() V33() Element of REAL
f . ((i + k1) - 1) is set
i - 1 is ext-real V14() V32() V33() Element of REAL
(i - 1) + k1 is ext-real V14() V32() V33() Element of REAL
f . ((i - 1) + k1) is set
1 + k1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(1 + k1) - 1 is ext-real V14() V32() V33() Element of REAL
1 - 1 is ext-real V14() V32() V33() Element of REAL
len (D,f,k1,k2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal set
(D,f,1,k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,1,k1) . k2 is set
f . k2 is set
k1 - 1 is ext-real V14() V32() V33() Element of REAL
(k1 - 1) + 1 is ext-real V14() V32() V33() Element of REAL
k2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f . ((k2 + 1) -' 1) is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,k1,k2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 - k1 is ext-real V14() V32() V33() set
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 - k1) + 1 is ext-real V14() V32() V33() Element of REAL
k1 - 1 is ext-real V14() V32() V33() Element of REAL
k2 - (k1 - 1) is ext-real V14() V32() V33() Element of REAL
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 + (k1 -' 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 - (k1 -' 1) is ext-real V14() V32() V33() set
(k2 + (k1 -' 1)) - (k1 -' 1) is ext-real V14() V32() V33() Element of REAL
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f | k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k2 is Element of D
<*k2*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
<*k2*> ^ f is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*k2*> ^ f) | (k1 + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k2*> ^ (f | k1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg k1 is V34() k1 -element Element of bool NAT
f | (Seg k1) is Relation-like NAT -defined Seg k1 -defined NAT -defined Seg k1 -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,D:]
[:NAT,D:] is Relation-like V34() set
bool [:NAT,D:] is V34() set
Seg (k1 + 1) is non empty V34() k1 + 1 -element Element of bool NAT
(<*k2*> ^ f) | (Seg (k1 + 1)) is Relation-like NAT -defined Seg (k1 + 1) -defined NAT -defined Seg (k1 + 1) -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,D:]
len <*k2*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 + (len <*k2*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
Seg (k1 + (len <*k2*>)) is non empty V34() k1 + (len <*k2*>) -element Element of bool NAT
(<*k2*> ^ f) | (Seg (k1 + (len <*k2*>))) is Relation-like NAT -defined Seg (k1 + (len <*k2*>)) -defined NAT -defined Seg (k1 + (len <*k2*>)) -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like Element of bool [:NAT,D:]
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
dom f is Element of bool NAT
k2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,k1,k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f . k1 is set
<*(f . k1)*> is non empty trivial Relation-like NAT -defined Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like set
k1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(D,f,(k1 + 1),k2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f . k1)*> ^ (D,f,(k1 + 1),k2) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
k2 -' k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
1 + k1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 -' k1) + k1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
k2 - k1 is ext-real V14() V32() V33() set
(k2 -' k1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k2 - k1) - 1 is ext-real V14() V32() V33() Element of REAL
k2 - (k1 + 1) is ext-real V14() V32() V33() Element of REAL
k2 -' (k1 + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /. k1 is Element of D
k1 -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(k1 -' 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. k1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() 1 -element FinSequence-like FinSubsequence-like FinSequence of D
f /^ k1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. k1)*> ^ (f /^ k1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(k2 -' k1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(<*(f /. k1)*> ^ (f /^ k1)) | ((k2 -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ k1) | (k2 -' k1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f . k1)*> ^ ((f /^ k1) | (k2 -' k1)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k2 -' (k1 + 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
(f /^ k1) | ((k2 -' (k1 + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f . k1)*> ^ ((f /^ k1) | ((k2 -' (k1 + 1)) + 1)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k1 + 1) -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
f /^ ((k1 + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ ((k1 + 1) -' 1)) | ((k2 -' (k1 + 1)) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f . k1)*> ^ ((f /^ ((k1 + 1) -' 1)) | ((k2 -' (k1 + 1)) + 1)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set