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