:: FINSEQ_6 semantic presentation

REAL is set
NAT is non empty V7() V8() V9() V34() cardinal limit_cardinal Element of bool REAL

NAT is non empty V7() V8() V9() V34() cardinal limit_cardinal set
bool NAT is V34() set
bool NAT is V34() set

RAT is set
INT is 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

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

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

D is set
f is set
k1 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 is non empty Element of bool NAT
D is set
f is set

rng <*D,f*> is non empty set
{D,f} 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
rng <*D*> is non empty trivial 1 -element set
rng <*f*> is non empty trivial 1 -element set
() \/ () is non empty set
{D} is non empty trivial 1 -element set
{D} \/ () 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

rng <*D,f,k1*> is non empty set
{D,f,k1} is 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) . 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

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

f 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
dom (<*D,f*> | (Seg 1)) is Element of bool NAT
(dom <*D,f*>) /\ (Seg 1) is Element of bool NAT

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

f is set
k1 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
dom (<*D,f,k1*> | (Seg 1)) is Element of bool NAT
(dom <*D,f,k1*>) /\ (Seg 1) is Element of bool NAT

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

k1 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
dom (<*D,f,k1*> | (Seg 2)) is Element of bool NAT
(dom <*D,f,k1*>) /\ (Seg 2) is Element of bool NAT

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

rng D is 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

rng D is set

rng f is set
(rng D) \ (rng f) is Element of bool (rng D)
bool (rng D) is 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

rng D is set

k1 is 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

rng D is set

rng f is set
(rng D) \ (rng f) is Element of bool (rng D)
bool (rng D) is set

k1 is 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

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

dom D is Element of bool NAT

rng D is set

k1 is 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

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

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

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

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

len D 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 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

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

rng D is set

rng f is set
(rng D) \ (rng f) is Element of bool (rng D)
bool (rng D) is set

k1 is 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

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

rng D is 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

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

rng D is set

k1 is 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 .. <*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 .. <*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

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 .. <*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

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

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 set

f is 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 is set

f is set
k1 is 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 is set
f is set
k1 is 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 is set
f is 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
() + (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

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 .. <*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 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 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

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

rng k1 is set

rng (k1 -| D) is 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

(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

rng f is 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

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 f) is Element of bool ()
bool () is set

rng (f ^ <*D*>) is non empty set
(rng f) \/ () 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) + () is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
D 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
rng f is 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)) + () is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() cardinal Element of NAT
((len (f -| 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

rng (Rev (f |-- D)) is 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)) ^ (<*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
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

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

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

rng f is set

rng (f -| D) is set

rng (Rev (f -| D)) is set

rng ((Rev f) |-- D) is set
rng (Rev f) is set
D is non empty set
f is Element 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

D is non empty set
f is Element 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 .. k1) is Relation-like NAT -defined