:: FINSEQ_8 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() V33() V38() V39() Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
NAT is non empty V4() V5() V6() V33() V38() V39() set
K6(NAT) is V33() set
K6(NAT) is V33() set
{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() functional V33() V38() V40( {} ) FinSequence-membered set
1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
3 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() functional V33() V38() V40( {} ) FinSequence-membered Element of NAT
D is set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f ^ CR is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
f ^ CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
rng (f ^ CR) is set
rng f is set
rng CR is set
(rng f) \/ (rng CR) is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
mid ((D,f,CR),1,(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) - 1 is V11() ext-real V15() set
(len f) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
1 - 1 is V11() ext-real V15() set
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len f) is V33() V40( len f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
(D,f,CR) | (Seg (len f)) is Relation-like FinSubsequence-like set
(D,f,CR) /^ 0 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((D,f,CR) /^ 0) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((D,f,CR) /^ 0) | (Seg (len f)) is Relation-like FinSubsequence-like set
D is set
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() Relation-like NAT -defined D -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) - CR is V11() ext-real V15() set
D is non empty set
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() Relation-like NAT -defined D -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid ((<*> D),f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR -' f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(CR -' f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(<*> D) /^ (f -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((<*> D) /^ (f -' 1)) | ((CR -' f) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((CR -' f) + 1) is non empty V33() V40((CR -' f) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR -' f) + 1 ) } is set
((<*> D) /^ (f -' 1)) | (Seg ((CR -' f) + 1)) is Relation-like FinSubsequence-like set
(<*> D) | ((CR -' f) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(<*> D) | (Seg ((CR -' f) + 1)) is Relation-like FinSubsequence-like set
f -' CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(f -' CR) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
CR -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(<*> D) /^ (CR -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((<*> D) /^ (CR -' 1)) | ((f -' CR) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((f -' CR) + 1) is non empty V33() V40((f -' CR) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (f -' CR) + 1 ) } is set
((<*> D) /^ (CR -' 1)) | (Seg ((f -' CR) + 1)) is Relation-like FinSubsequence-like set
Rev (((<*> D) /^ (CR -' 1)) | ((f -' CR) + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(<*> D) | ((f -' CR) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(<*> D) | (Seg ((f -' CR) + 1)) is Relation-like FinSubsequence-like set
Rev ((<*> D) | ((f -' CR) + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Rev (<*> D) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
(CR + 1) -' f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
D /^ (f -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(D /^ (f -' 1)) | ((CR + 1) -' f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((CR + 1) -' f) is V33() V40((CR + 1) -' f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR + 1) -' f ) } is set
(D /^ (f -' 1)) | (Seg ((CR + 1) -' f)) is Relation-like FinSubsequence-like set
D is set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
(f,CR,n) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(n + 1) -' CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (CR -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (CR -' 1)) | ((n + 1) -' CR) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((n + 1) -' CR) is V33() V40((n + 1) -' CR) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (n + 1) -' CR ) } is set
(f /^ (CR -' 1)) | (Seg ((n + 1) -' CR)) is Relation-like FinSubsequence-like set
f /^ (CR -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (CR -' 1)) | ((n + 1) -' CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (CR -' 1)) | (Seg ((n + 1) -' CR)) is Relation-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(CR + 1) -' f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D /^ (f -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(D /^ (f -' 1)) | ((CR + 1) -' f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((CR + 1) -' f) is V33() V40((CR + 1) -' f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR + 1) -' f ) } is set
(D /^ (f -' 1)) | (Seg ((CR + 1) -' f)) is Relation-like FinSubsequence-like set
mid (D,f,CR) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
CR -' f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(CR -' f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
CR - f is V11() ext-real V15() set
(CR - f) + 1 is V11() ext-real V15() set
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(CR + 1) - f is V11() ext-real V15() set
(CR + 1) -' f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,1,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(CR + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (1 -' 1)) | ((CR + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((CR + 1) -' 1) is V33() V40((CR + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR + 1) -' 1 ) } is set
(f /^ (1 -' 1)) | (Seg ((CR + 1) -' 1)) is Relation-like FinSubsequence-like set
f | CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg CR is V33() V40(CR) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= CR ) } is set
f | (Seg CR) is Relation-like FinSubsequence-like set
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(CR + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ 0 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 0) | ((CR + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((CR + 1) -' 1) is V33() V40((CR + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR + 1) -' 1 ) } is set
(f /^ 0) | (Seg ((CR + 1) -' 1)) is Relation-like FinSubsequence-like set
f | ((CR + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f | (Seg ((CR + 1) -' 1)) is Relation-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,1,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(CR + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (1 -' 1)) | ((CR + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((CR + 1) -' 1) is V33() V40((CR + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR + 1) -' 1 ) } is set
(f /^ (1 -' 1)) | (Seg ((CR + 1) -' 1)) is Relation-like FinSubsequence-like set
f | CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg CR is V33() V40(CR) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= CR ) } is set
f | (Seg CR) is Relation-like FinSubsequence-like set
D is set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR,n) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(n + 1) -' CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (CR -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (CR -' 1)) | ((n + 1) -' CR) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((n + 1) -' CR) is V33() V40((n + 1) -' CR) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (n + 1) -' CR ) } is set
(f /^ (CR -' 1)) | (Seg ((n + 1) -' CR)) is Relation-like FinSubsequence-like set
f /^ (CR -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
k1 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 | 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() Relation-like NAT -defined D -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
Seg 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() functional V33() V38() V40( 0 ) V40( {} ) FinSequence-membered Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= 0 ) } is set
k1 | (Seg 0) is Relation-like FinSubsequence-like set
D is set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,0,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(CR + 1) -' 0 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (0 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (0 -' 1)) | ((CR + 1) -' 0) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((CR + 1) -' 0) is V33() V40((CR + 1) -' 0) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR + 1) -' 0 ) } is set
(f /^ (0 -' 1)) | (Seg ((CR + 1) -' 0)) is Relation-like FinSubsequence-like set
CR + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,1,(CR + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR + 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((CR + 1) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (1 -' 1)) | (((CR + 1) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((CR + 1) + 1) -' 1) is V33() V40(((CR + 1) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((CR + 1) + 1) -' 1 ) } is set
(f /^ (1 -' 1)) | (Seg (((CR + 1) + 1) -' 1)) is Relation-like FinSubsequence-like set
(CR + 1) -' 0 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ 0 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 0) | ((CR + 1) -' 0) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((CR + 1) -' 0) is V33() V40((CR + 1) -' 0) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (CR + 1) -' 0 ) } is set
(f /^ 0) | (Seg ((CR + 1) -' 0)) is Relation-like FinSubsequence-like set
f | ((CR + 1) -' 0) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f | (Seg ((CR + 1) -' 0)) is Relation-like FinSubsequence-like set
f | (CR + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (CR + 1) is non empty V33() V40(CR + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= CR + 1 ) } is set
f | (Seg (CR + 1)) is Relation-like FinSubsequence-like set
(CR + 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((CR + 1) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f | (((CR + 1) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((CR + 1) + 1) -' 1) is V33() V40(((CR + 1) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((CR + 1) + 1) -' 1 ) } is set
f | (Seg (((CR + 1) + 1) -' 1)) is Relation-like FinSubsequence-like set
(f /^ 0) | (((CR + 1) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 0) | (Seg (((CR + 1) + 1) -' 1)) is Relation-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,(D,f,CR),((len f) + 1),((len f) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + (len CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((len f) + (len CR)) + 1) -' ((len f) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR) /^ (((len f) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((D,f,CR) /^ (((len f) + 1) -' 1)) | ((((len f) + (len CR)) + 1) -' ((len f) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((((len f) + (len CR)) + 1) -' ((len f) + 1)) is V33() V40((((len f) + (len CR)) + 1) -' ((len f) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((len f) + (len CR)) + 1) -' ((len f) + 1) ) } is set
((D,f,CR) /^ (((len f) + 1) -' 1)) | (Seg ((((len f) + (len CR)) + 1) -' ((len f) + 1))) is Relation-like FinSubsequence-like set
(len CR) + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len CR) + (len f)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((len CR) + (len f)) + 1) -' ((len f) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len CR) + ((len f) + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len CR) + ((len f) + 1)) -' ((len f) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR | ((((len CR) + (len f)) + 1) -' ((len f) + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((len CR) + (len f)) + 1) -' ((len f) + 1)) is V33() V40((((len CR) + (len f)) + 1) -' ((len f) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((len CR) + (len f)) + 1) -' ((len f) + 1) ) } is set
CR | (Seg ((((len CR) + (len f)) + 1) -' ((len f) + 1))) is Relation-like FinSubsequence-like set
((len f) + (len CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((len f) + (len CR)) + 1) -' ((len f) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR) /^ (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((D,f,CR) /^ (len f)) | ((((len f) + (len CR)) + 1) -' ((len f) + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((len f) + (len CR)) + 1) -' ((len f) + 1)) is V33() V40((((len f) + (len CR)) + 1) -' ((len f) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((len f) + (len CR)) + 1) -' ((len f) + 1) ) } is set
((D,f,CR) /^ (len f)) | (Seg ((((len f) + (len CR)) + 1) -' ((len f) + 1))) is Relation-like FinSubsequence-like set
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,CR,1,0) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(0 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(CR /^ (1 -' 1)) | ((0 + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((0 + 1) -' 1) is V33() V40((0 + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (0 + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg ((0 + 1) -' 1)) is Relation-like FinSubsequence-like set
(len f) -' 0 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' 0) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len f) - 0 is V11() ext-real non negative V15() set
((len f) - 0) + 1 is non empty V11() ext-real positive non negative V15() set
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' 0) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (((len f) -' 0) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' 0) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' 0) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' 0) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' 0) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' 0) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' 0) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' 0) + 1) ) } is set
(f /^ ((((len f) -' 0) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' 0) + 1))) is Relation-like FinSubsequence-like set
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
(D,CR,1,n) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(n + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(CR /^ (1 -' 1)) | ((n + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((n + 1) -' 1) is V33() V40((n + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (n + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg ((n + 1) -' 1)) is Relation-like FinSubsequence-like set
(len f) -' n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' n) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' n) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + 1) -' (((len f) -' n) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' n) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' n) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' n) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' n) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' n) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' n) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' n) + 1) ) } is set
(f /^ ((((len f) -' n) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' n) + 1))) is Relation-like FinSubsequence-like set
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
(D,CR,1,n) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(n + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(CR /^ (1 -' 1)) | ((n + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((n + 1) -' 1) is V33() V40((n + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (n + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg ((n + 1) -' 1)) is Relation-like FinSubsequence-like set
(len f) -' n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' n) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' n) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + 1) -' (((len f) -' n) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' n) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' n) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' n) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' n) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' n) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' n) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' n) + 1) ) } is set
(f /^ ((((len f) -' n) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' n) + 1))) is Relation-like FinSubsequence-like set
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,CR,1,k1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(k1 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(CR /^ (1 -' 1)) | ((k1 + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((k1 + 1) -' 1) is V33() V40((k1 + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (k1 + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg ((k1 + 1) -' 1)) is Relation-like FinSubsequence-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
mid (CR,1,k1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,CR,1,k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
k1 - 1 is V11() ext-real V15() set
(k1 - 1) + 1 is V11() ext-real V15() set
len (D,CR,1,k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (D,CR,1,k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (D,CR,1,k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (D,CR,1,k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (D,CR,1,k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,CR,1,(len n)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len n) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len n) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(CR /^ (1 -' 1)) | (((len n) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len n) + 1) -' 1) is V33() V40(((len n) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len n) + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg (((len n) + 1) -' 1)) is Relation-like FinSubsequence-like set
(len f) -' (len n) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len n)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' (len n)) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (((len f) -' (len n)) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len n)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' (len n)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' (len n)) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' (len n)) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' (len n)) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' (len n)) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' (len n)) + 1) ) } is set
(f /^ ((((len f) -' (len n)) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' (len n)) + 1))) is Relation-like FinSubsequence-like set
k1 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,CR,1,(len k1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len k1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len k1) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(CR /^ (1 -' 1)) | (((len k1) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len k1) + 1) -' 1) is V33() V40(((len k1) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len k1) + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg (((len k1) + 1) -' 1)) is Relation-like FinSubsequence-like set
(len f) -' (len k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len k1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' (len k1)) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + 1) -' (((len f) -' (len k1)) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len k1)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' (len k1)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' (len k1)) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' (len k1)) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' (len k1)) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' (len k1)) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' (len k1)) + 1) ) } is set
(f /^ ((((len f) -' (len k1)) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' (len k1)) + 1))) is Relation-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) - (len (D,f,CR)) is V11() ext-real V15() set
(len f) -' (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len (D,f,CR))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' (len (D,f,CR))) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len (D,f,CR))) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1) ) } is set
(f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1))) is Relation-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) -' (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f | ((len f) -' (len (D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len f) -' (len (D,f,CR))) is V33() V40((len f) -' (len (D,f,CR))) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (len f) -' (len (D,f,CR)) ) } is set
f | (Seg ((len f) -' (len (D,f,CR)))) is Relation-like FinSubsequence-like set
(D,(f | ((len f) -' (len (D,f,CR)))),CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) - (len (D,f,CR)) is V11() ext-real V15() set
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) + (len (D,f,CR)) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) - (len (D,f,CR)) is V11() ext-real V15() set
(((len f) + 1) + (len (D,f,CR))) - (len (D,f,CR)) is V11() ext-real V15() set
((len f) -' (len (D,f,CR))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) + 1) - (((len f) -' (len (D,f,CR))) + 1) is V11() ext-real V15() set
f /^ ((len f) -' (len (D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ ((len f) -' (len (D,f,CR)))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) - ((len f) -' (len (D,f,CR))) is V11() ext-real V15() set
0 + (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' (len (D,f,CR))) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len (D,f,CR))) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1) ) } is set
(f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1))) is Relation-like FinSubsequence-like set
(f /^ ((len f) -' (len (D,f,CR)))) | (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len (D,f,CR)) is V33() V40( len (D,f,CR)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len (D,f,CR) ) } is set
(f /^ ((len f) -' (len (D,f,CR)))) | (Seg (len (D,f,CR))) is Relation-like FinSubsequence-like set
(D,CR,1,(len (D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len (D,f,CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len (D,f,CR)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(CR /^ (1 -' 1)) | (((len (D,f,CR)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len (D,f,CR)) + 1) -' 1) is V33() V40(((len (D,f,CR)) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len (D,f,CR)) + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg (((len (D,f,CR)) + 1) -' 1)) is Relation-like FinSubsequence-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(0 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ ((0 + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ ((0 + 1) -' 1)) | (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ ((0 + 1) -' 1)) | (Seg (len (D,f,CR))) is Relation-like FinSubsequence-like set
CR /^ 0 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ 0) | (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ 0) | (Seg (len (D,f,CR))) is Relation-like FinSubsequence-like set
CR | (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR | (Seg (len (D,f,CR))) is Relation-like FinSubsequence-like set
(D,(f | ((len f) -' (len (D,f,CR)))),(CR | (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(f | ((len f) -' (len (D,f,CR)))),(CR | (len (D,f,CR)))),(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(CR | (len (D,f,CR))),(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f | ((len f) -' (len (D,f,CR)))),(D,(CR | (len (D,f,CR))),(CR /^ (len (D,f,CR))))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) -' (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f | ((len f) -' (len (D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len f) -' (len (D,f,CR))) is V33() V40((len f) -' (len (D,f,CR))) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (len f) -' (len (D,f,CR)) ) } is set
f | (Seg ((len f) -' (len (D,f,CR)))) is Relation-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) -' (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f | ((len f) -' (len (D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len f) -' (len (D,f,CR))) is V33() V40((len f) -' (len (D,f,CR))) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (len f) -' (len (D,f,CR)) ) } is set
f | (Seg ((len f) -' (len (D,f,CR)))) is Relation-like FinSubsequence-like set
(D,(D,f,CR),(D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,CR),(D,f,CR)),(D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,CR),(D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,CR),(D,(D,f,CR),(D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,CR),(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,CR,1,(len (D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len (D,f,CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len (D,f,CR)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(CR /^ (1 -' 1)) | (((len (D,f,CR)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len (D,f,CR)) + 1) -' 1) is V33() V40(((len (D,f,CR)) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len (D,f,CR)) + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg (((len (D,f,CR)) + 1) -' 1)) is Relation-like FinSubsequence-like set
(D,(D,CR,1,(len (D,f,CR))),(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR | (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len (D,f,CR)) is V33() V40( len (D,f,CR)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len (D,f,CR) ) } is set
CR | (Seg (len (D,f,CR))) is Relation-like FinSubsequence-like set
(D,(CR | (len (D,f,CR))),(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f | ((len f) -' (len (D,f,CR)))),(D,(D,f,CR),(CR /^ (len (D,f,CR))))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (len (D,f,f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(f /^ (len (D,f,f)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) -' (len (D,f,f)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f | ((len f) -' (len (D,f,f))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len f) -' (len (D,f,f))) is V33() V40((len f) -' (len (D,f,f))) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (len f) -' (len (D,f,f)) ) } is set
f | (Seg ((len f) -' (len (D,f,f)))) is Relation-like FinSubsequence-like set
(D,f,f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,1,(len (D,f,f))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len (D,f,f)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len (D,f,f)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (1 -' 1)) | (((len (D,f,f)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len (D,f,f)) + 1) -' 1) is V33() V40(((len (D,f,f)) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len (D,f,f)) + 1) -' 1 ) } is set
(f /^ (1 -' 1)) | (Seg (((len (D,f,f)) + 1) -' 1)) is Relation-like FinSubsequence-like set
(len f) -' (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len f)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len f) - (len f) is V11() ext-real V15() set
((len f) - (len f)) + 1 is V11() ext-real V15() set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,1,(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(f /^ (1 -' 1)) | (((len f) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' 1) is V33() V40(((len f) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' 1 ) } is set
(f /^ (1 -' 1)) | (Seg (((len f) + 1) -' 1)) is Relation-like FinSubsequence-like set
(D,f,(((len f) -' (len f)) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + 1) -' (((len f) -' (len f)) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len f)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' (len f)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' (len f)) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' (len f)) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' (len f)) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' (len f)) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' (len f)) + 1) ) } is set
(f /^ ((((len f) -' (len f)) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' (len f)) + 1))) is Relation-like FinSubsequence-like set
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() Relation-like NAT -defined D -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
(D,f,(<*> D)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f | ((len f) -' (len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len f) -' (len f)) is V33() V40((len f) -' (len f)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (len f) -' (len f) ) } is set
f | (Seg ((len f) -' (len f))) is Relation-like FinSubsequence-like set
f | 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() Relation-like NAT -defined D -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
Seg 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() functional V33() V38() V40( 0 ) V40( {} ) FinSequence-membered Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= 0 ) } is set
f | (Seg 0) is Relation-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,CR),CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,(D,f,CR),CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,CR,1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len CR) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len CR) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(CR /^ (1 -' 1)) | (((len CR) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len CR) + 1) -' 1) is V33() V40(((len CR) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len CR) + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg (((len CR) + 1) -' 1)) is Relation-like FinSubsequence-like set
CR | (len CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len CR) is V33() V40( len CR) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len CR ) } is set
CR | (Seg (len CR)) is Relation-like FinSubsequence-like set
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (D,f,CR)) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len (D,f,CR)) -' (len CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) + (len CR)) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) + (len CR)) -' (len CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,(D,f,CR),(((len (D,f,CR)) -' (len CR)) + 1),(len (D,f,CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len (D,f,CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len (D,f,CR)) + 1) -' (((len (D,f,CR)) -' (len CR)) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len (D,f,CR)) -' (len CR)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR) /^ ((((len (D,f,CR)) -' (len CR)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((D,f,CR) /^ ((((len (D,f,CR)) -' (len CR)) + 1) -' 1)) | (((len (D,f,CR)) + 1) -' (((len (D,f,CR)) -' (len CR)) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len (D,f,CR)) + 1) -' (((len (D,f,CR)) -' (len CR)) + 1)) is V33() V40(((len (D,f,CR)) + 1) -' (((len (D,f,CR)) -' (len CR)) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len (D,f,CR)) + 1) -' (((len (D,f,CR)) -' (len CR)) + 1) ) } is set
((D,f,CR) /^ ((((len (D,f,CR)) -' (len CR)) + 1) -' 1)) | (Seg (((len (D,f,CR)) + 1) -' (((len (D,f,CR)) -' (len CR)) + 1))) is Relation-like FinSubsequence-like set
(D,(D,f,CR),((len f) + 1),((len f) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + (len CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((len f) + (len CR)) + 1) -' ((len f) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR) /^ (((len f) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((D,f,CR) /^ (((len f) + 1) -' 1)) | ((((len f) + (len CR)) + 1) -' ((len f) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((((len f) + (len CR)) + 1) -' ((len f) + 1)) is V33() V40((((len f) + (len CR)) + 1) -' ((len f) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((len f) + (len CR)) + 1) -' ((len f) + 1) ) } is set
((D,f,CR) /^ (((len f) + 1) -' 1)) | (Seg ((((len f) + (len CR)) + 1) -' ((len f) + 1))) is Relation-like FinSubsequence-like set
(D,CR,1,(len (D,(D,f,CR),CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len (D,(D,f,CR),CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len (D,(D,f,CR),CR)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(CR /^ (1 -' 1)) | (((len (D,(D,f,CR),CR)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len (D,(D,f,CR),CR)) + 1) -' 1) is V33() V40(((len (D,(D,f,CR),CR)) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len (D,(D,f,CR),CR)) + 1) -' 1 ) } is set
(CR /^ (1 -' 1)) | (Seg (((len (D,(D,f,CR),CR)) + 1) -' 1)) is Relation-like FinSubsequence-like set
len (D,f,(D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) -' (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len f)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' (len f)) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (((len f) -' (len f)) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len f)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' (len f)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' (len f)) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' (len f)) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' (len f)) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' (len f)) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' (len f)) + 1) ) } is set
(f /^ ((((len f) -' (len f)) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' (len f)) + 1))) is Relation-like FinSubsequence-like set
(0 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((0 + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ ((0 + 1) -' 1)) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len f) is V33() V40( len f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
(f /^ ((0 + 1) -' 1)) | (Seg (len f)) is Relation-like FinSubsequence-like set
f /^ 0 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 0) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ 0) | (Seg (len f)) is Relation-like FinSubsequence-like set
f | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f | (Seg (len f)) is Relation-like FinSubsequence-like set
(D,(D,f,CR),1,(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,CR) /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((D,f,CR) /^ (1 -' 1)) | (((len f) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' 1) is V33() V40(((len f) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' 1 ) } is set
((D,f,CR) /^ (1 -' 1)) | (Seg (((len f) + 1) -' 1)) is Relation-like FinSubsequence-like set
(D,f,CR) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) | (Seg (len f)) is Relation-like FinSubsequence-like set
(D,(D,f,CR),1,(len (D,f,(D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len (D,f,(D,f,CR))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len (D,f,(D,f,CR))) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((D,f,CR) /^ (1 -' 1)) | (((len (D,f,(D,f,CR))) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len (D,f,(D,f,CR))) + 1) -' 1) is V33() V40(((len (D,f,(D,f,CR))) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len (D,f,(D,f,CR))) + 1) -' 1 ) } is set
((D,f,CR) /^ (1 -' 1)) | (Seg (((len (D,f,(D,f,CR))) + 1) -' 1)) is Relation-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) + (len CR)) - (len (D,f,CR)) is V11() ext-real V15() set
((len f) + (len CR)) -' (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len CR) -' (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + ((len CR) -' (len (D,f,CR))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (CR /^ (len (D,f,CR))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + (len (CR /^ (len (D,f,CR)))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len CR) - (len (D,f,CR)) is V11() ext-real V15() set
(len f) + ((len CR) - (len (D,f,CR))) is V11() ext-real V15() set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) -' (len (D,f,CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len (D,f,CR))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(((len f) -' (len (D,f,CR))) + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len (D,f,CR))) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1)) | (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) is V33() V40(((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1) ) } is set
(f /^ ((((len f) -' (len (D,f,CR))) + 1) -' 1)) | (Seg (((len f) + 1) -' (((len f) -' (len (D,f,CR))) + 1))) is Relation-like FinSubsequence-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,f,(0 + 1),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) + 1) -' (0 + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(0 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ ((0 + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ ((0 + 1) -' 1)) | (((len f) + 1) -' (0 + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len f) + 1) -' (0 + 1)) is V33() V40(((len f) + 1) -' (0 + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' (0 + 1) ) } is set
(f /^ ((0 + 1) -' 1)) | (Seg (((len f) + 1) -' (0 + 1))) is Relation-like FinSubsequence-like set
D is non empty set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f /^ 1 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f /^ 1),f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,(f /^ 1),f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f | 1 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg 1 is non empty V2() V33() V40(1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
f | (Seg 1) is Relation-like FinSubsequence-like set
(D,(f /^ 1),f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f /^ (len (D,(f /^ 1),f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f /^ 1),(f /^ (len (D,(f /^ 1),f)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f | 1),(D,(f /^ 1),f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f | 1),(f /^ 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(f | 1),(f /^ 1)),(f /^ (len (D,(f /^ 1),f)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(f /^ (len (D,(f /^ 1),f)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (f /^ 1)) -' (len (D,(f /^ 1),f)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len (f /^ 1)) -' (len (D,(f /^ 1),f))) is V33() V40((len (f /^ 1)) -' (len (D,(f /^ 1),f))) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (len (f /^ 1)) -' (len (D,(f /^ 1),f)) ) } is set
(f /^ 1) | (Seg ((len (f /^ 1)) -' (len (D,(f /^ 1),f)))) is Relation-like FinSubsequence-like set
(D,((f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f)))),f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f | 1),(D,((f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f)))),f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f | 1),((f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f))))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(f | 1),((f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f))))),f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,(f | 1),((f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f))))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (f | 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len ((f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f)))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (f | 1)) + (len ((f /^ 1) | ((len (f /^ 1)) -' (len (D,(f /^ 1),f))))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (f | 1)) + ((len (f /^ 1)) -' (len (D,(f /^ 1),f))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (f /^ 1)) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
(len (f | 1)) + ((len (f /^ 1)) - (len (D,(f /^ 1),f))) is V11() ext-real V15() set
(len (f | 1)) + (len (f /^ 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len (f | 1)) + (len (f /^ 1))) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
len (D,(f | 1),(f /^ 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (D,(f | 1),(f /^ 1))) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
(len f) -' (len (D,(f /^ 1),f)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (D,(f | 1),(D,(f /^ 1),f)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (D,(f /^ 1),f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (f | 1)) + (len (D,(f /^ 1),f)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len (f /^ 1)) + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len (f /^ 1)) + (len f)) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
(len (f | 1)) + (((len (f /^ 1)) + (len f)) - (len (D,(f /^ 1),f))) is V11() ext-real V15() set
((len (f | 1)) + (len (f /^ 1))) + ((len f) - (len (D,(f /^ 1),f))) is V11() ext-real V15() set
(len (D,(f | 1),(f /^ 1))) + ((len f) - (len (D,(f /^ 1),f))) is V11() ext-real V15() set
(len f) + ((len f) - (len (D,(f /^ 1),f))) is V11() ext-real V15() set
((len f) + 1) -' (len (D,(f /^ 1),f)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 + (len f) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(1 + (len f)) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
1 + ((len f) - (len (D,(f /^ 1),f))) is V11() ext-real V15() set
1 + ((len f) -' (len (D,(f /^ 1),f))) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(1 + (len f)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,(D,(f | 1),(D,(f /^ 1),f)),1,((1 + (len f)) -' 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((1 + (len f)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((1 + (len f)) -' 1) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,(f | 1),(D,(f /^ 1),f)) /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((D,(f | 1),(D,(f /^ 1),f)) /^ (1 -' 1)) | ((((1 + (len f)) -' 1) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((((1 + (len f)) -' 1) + 1) -' 1) is V33() V40((((1 + (len f)) -' 1) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((1 + (len f)) -' 1) + 1) -' 1 ) } is set
((D,(f | 1),(D,(f /^ 1),f)) /^ (1 -' 1)) | (Seg ((((1 + (len f)) -' 1) + 1) -' 1)) is Relation-like FinSubsequence-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(0 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,(f | 1),(D,(f /^ 1),f)) /^ ((0 + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((D,(f | 1),(D,(f /^ 1),f)) /^ ((0 + 1) -' 1)) | (((len f) + 1) -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len f) + 1) -' 1) is V33() V40(((len f) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) + 1) -' 1 ) } is set
((D,(f | 1),(D,(f /^ 1),f)) /^ ((0 + 1) -' 1)) | (Seg (((len f) + 1) -' 1)) is Relation-like FinSubsequence-like set
(D,(f | 1),(D,(f /^ 1),f)) /^ 0 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((D,(f | 1),(D,(f /^ 1),f)) /^ 0) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len f) is V33() V40( len f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
((D,(f | 1),(D,(f /^ 1),f)) /^ 0) | (Seg (len f)) is Relation-like FinSubsequence-like set
(D,(f | 1),(D,(f /^ 1),f)) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,(f | 1),(D,(f /^ 1),f)) | (Seg (len f)) is Relation-like FinSubsequence-like set
(((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) - 1 is V11() ext-real V15() set
(((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) - 1) + 1 is V11() ext-real V15() set
((((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1) -' (((len f) + 1) -' (len (D,(f /^ 1),f))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) - (((len f) + 1) -' (len (D,(f /^ 1),f))) is V11() ext-real V15() set
(((len f) + 1) -' (len (D,(f /^ 1),f))) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) + 1) -' (len (D,(f /^ 1),f))) - 1 is V11() ext-real V15() set
((len f) + 1) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
(((len f) + 1) - (len (D,(f /^ 1),f))) - 1 is V11() ext-real V15() set
((len f) + 1) - 1 is V11() ext-real V15() set
(((len f) + 1) - 1) - (len (D,(f /^ 1),f)) is V11() ext-real V15() set
(D,(D,(f | 1),(D,(f /^ 1),f)),(((len f) + 1) -' (len (D,(f /^ 1),f))),(((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1) -' (((len f) + 1) -' (len (D,(f /^ 1),f))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,(f | 1),(D,(f /^ 1),f)) /^ ((((len f) + 1) -' (len (D,(f /^ 1),f))) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((D,(f | 1),(D,(f /^ 1),f)) /^ ((((len f) + 1) -' (len (D,(f /^ 1),f))) -' 1)) | (((((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1) -' (((len f) + 1) -' (len (D,(f /^ 1),f)))) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1) -' (((len f) + 1) -' (len (D,(f /^ 1),f)))) is V33() V40(((((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1) -' (((len f) + 1) -' (len (D,(f /^ 1),f)))) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1) -' (((len f) + 1) -' (len (D,(f /^ 1),f))) ) } is set
((D,(f | 1),(D,(f /^ 1),f)) /^ ((((len f) + 1) -' (len (D,(f /^ 1),f))) -' 1)) | (Seg (((((((len f) + 1) -' (len (D,(f /^ 1),f))) + (len f)) -' 1) + 1) -' (((len f) + 1) -' (len (D,(f /^ 1),f))))) is Relation-like FinSubsequence-like set
f | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f | (Seg (len f)) is Relation-like FinSubsequence-like set
(len f) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(1 + (len f)) - ((len f) -' 1) is V11() ext-real V15() set
(len f) - 1 is V11() ext-real V15() set
(1 + (len f)) - ((len f) - 1) is V11() ext-real V15() set
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) -' (len (D,(f /^ 1),f))) + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (len (D,(f /^ 1),f))) + (len f)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((((len f) -' (len (D,(f /^ 1),f))) + (len f)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + ((len f) -' (len (D,(f /^ 1),f))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(1 + ((len f) -' (len (D,(f /^ 1),f)))) + (len f) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((1 + ((len f) -' (len (D,(f /^ 1),f)))) + (len f)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(1 + ((len f) -' (len (D,(f /^ 1),f)))) - 1 is V11() ext-real V15() set
n is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 + (len f)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 + (len f)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,n,k1,((k1 + (len f)) -' 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((k1 + (len f)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((k1 + (len f)) -' 1) + 1) -' k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n /^ (k1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(n /^ (k1 -' 1)) | ((((k1 + (len f)) -' 1) + 1) -' k1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((((k1 + (len f)) -' 1) + 1) -' k1) is V33() V40((((k1 + (len f)) -' 1) + 1) -' k1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((k1 + (len f)) -' 1) + 1) -' k1 ) } is set
(n /^ (k1 -' 1)) | (Seg ((((k1 + (len f)) -' 1) + 1) -' k1)) is Relation-like FinSubsequence-like set
(D,n,k2,((k2 + (len f)) -' 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((k2 + (len f)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((k2 + (len f)) -' 1) + 1) -' k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n /^ (k2 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(n /^ (k2 -' 1)) | ((((k2 + (len f)) -' 1) + 1) -' k2) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((((k2 + (len f)) -' 1) + 1) -' k2) is V33() V40((((k2 + (len f)) -' 1) + 1) -' k2) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((k2 + (len f)) -' 1) + 1) -' k2 ) } is set
(n /^ (k2 -' 1)) | (Seg ((((k2 + (len f)) -' 1) + 1) -' k2)) is Relation-like FinSubsequence-like set
k2 -' k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 - k1 is V11() ext-real V15() set
k1 + (k2 -' k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 - k1) + k1 is V11() ext-real V15() set
(len f) - 1 is V11() ext-real V15() set
(k1 + (len f)) - 1 is V11() ext-real V15() set
k1 + ((len f) -' 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 -' k1) - 1 is V11() ext-real V15() set
(k2 -' k1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 + ((k2 -' k1) -' 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 + ((k2 -' k1) - 1) is V11() ext-real V15() set
(k2 - k1) - 1 is V11() ext-real V15() set
k1 + ((k2 - k1) - 1) is V11() ext-real V15() set
k2 - 1 is V11() ext-real V15() set
k1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(k1 + 1) - 1 is V11() ext-real V15() set
(k2 -' 1) + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 - 1) + (len f) is V11() ext-real V15() set
(k2 + (len f)) - 1 is V11() ext-real V15() set
((k2 -' k1) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len f) - (k2 -' k1) is V11() ext-real V15() set
(k2 -' k1) - (k2 -' k1) is V11() ext-real V15() set
(len f) -' (k2 -' k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(1 + 1) - 1 is V11() ext-real V15() set
k2 + ((len f) - 1) is V11() ext-real V15() set
k2 + ((len f) -' 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 + 1) + (len f) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((k1 + 1) + (len f)) - 1 is V11() ext-real V15() set
((k1 + 1) - 1) + (len f) is V11() ext-real V15() set
(k1 + (len f)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
k2 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(k2 + 1) - 1 is V11() ext-real V15() set
(len f) + (k2 -' k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(D,f,1,((len f) -' (k2 -' k1))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) -' (k2 -' k1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(((len f) -' (k2 -' k1)) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f /^ (1 -' 1)) | ((((len f) -' (k2 -' k1)) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg ((((len f) -' (k2 -' k1)) + 1) -' 1) is V33() V40((((len f) -' (k2 -' k1)) + 1) -' 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((len f) -' (k2 -' k1)) + 1) -' 1 ) } is set
(f /^ (1 -' 1)) | (Seg ((((len f) -' (k2 -' k1)) + 1) -' 1)) is Relation-like FinSubsequence-like set
len (D,f,1,((len f) -' (k2 -' k1))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,1,((len f) -' (k2 -' k1))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (mid (f,1,((len f) -' (k2 -' k1)))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (k2 -' k1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' (k2 -' k1)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) -' (k2 -' k1)) - 1 is V11() ext-real V15() set
(((len f) -' (k2 -' k1)) - 1) + 1 is V11() ext-real V15() set
(len (f /^ 1)) -' ((len f) -' (k2 -' k1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) -' 1) -' ((len f) -' (k2 -' k1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' 1) -' ((len f) -' (k2 -' k1))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) -' 1) - ((len f) -' (k2 -' k1)) is V11() ext-real V15() set
(((len f) -' 1) - ((len f) -' (k2 -' k1))) + 1 is V11() ext-real V15() set
((len f) - 1) - ((len f) - (k2 -' k1)) is V11() ext-real V15() set
(((len f) - 1) - ((len f) - (k2 -' k1))) + 1 is V11() ext-real V15() set
(D,(f /^ 1),(((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1),(len (f /^ 1))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len (f /^ 1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len (f /^ 1)) + 1) -' (((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(f /^ 1) /^ ((((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1) -' 1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((f /^ 1) /^ ((((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1) -' 1)) | (((len (f /^ 1)) + 1) -' (((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Seg (((len (f /^ 1)) + 1) -' (((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1)) is V33() V40(((len (f /^ 1)) + 1) -' (((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len (f /^ 1)) + 1) -' (((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1) ) } is set
((f /^ 1) /^ ((((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1) -' 1)) | (Seg (((len (f /^ 1)) + 1) -' (((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1))) is Relation-like FinSubsequence-like set
mid ((f /^ 1),(k2 -' k1),((len f) -' 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (mid ((f /^ 1),(k2 -' k1),((len f) -' 1))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' 1) -' (k2 -' k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((len f) -' 1) -' (k2 -' k1)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) -' 1) - (k2 -' k1) is V11() ext-real V15() set
(((len f) -' 1) - (k2 -' k1)) + 1 is V11() ext-real V15() set
((len f) - 1) - (k2 -' k1) is V11() ext-real V15() set
(((len f) - 1) - (k2 -' k1)) + 1 is V11() ext-real V15() set
j is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
(D,f,1,((len f) -' (k2 -' k1))) . j is set
(D,(f /^ 1),(((len (f /^ 1)) -' ((len f) -' (k2 -' k1))) + 1),(len (f /^ 1))) . j is set
j + (k2 -' k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (k2 -' k1)) + (k2 -' k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(j + (k2 -' k1)) - 1 is V11() ext-real V15() set
mid (n,k1,((k1 + (len f)) -' 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (mid (n,k1,((k1 + (len f)) -' 1))) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((k1 + (len f)) -' 1) -' k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((k1 + (len f)) -' 1) -' k1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((k1 + (len f)) - 1) - k1 is V11() ext-real V15() set
(((k1 + (len f)) - 1) - k1) + 1 is V11() ext-real V15() set
j + ((k2 -' k1) -' 1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
j + ((k2 -' k1) - 1) is V11() ext-real V15() set
(j + (k2 -' k1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
Seg (len (f /^ 1)) is V33() V40( len (f /^ 1)) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len (f /^ 1) ) } is set
dom (f /^ 1) is Element of K6(NAT)
mid (n,k2,((k2 + (len f)) -' 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
j1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
j1 + (k2 -' k1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(j1 + (k2 -' k1)) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(f /^ 1) . ((j1 + (k2 -' k1)) -' 1) is set
((j + (k2 -' k1)) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(D,n,k1,((k1 + (len f)) -' 1)) . (((j + (k2 -' k1)) -' 1) + 1) is set
(mid (n,k1,((k1 + (len f)) -' 1))) . (((j + (k2 -' k1)) -' 1) + 1) is set
((j + (k2 -' k1)) - 1) + 1 is V11() ext-real V15() set
(mid (n,k1,((k1 + (len f)) -' 1))) . (((j + (k2 -' k1)) - 1) + 1) is set
k1 + (j1 + (k2 -' k1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 + (j1 + (k2 -' k1))) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n . ((k1 + (j1 + (k2 -' k1))) -' 1) is set
(k1 + (k2 -' k1)) + j1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((k1 + (k2 -' k1)) + j1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n . (((k1 + (k2 -' k1)) + j1) -' 1) is set
f . j is set
j1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(j1 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f . ((j1 + 1) -' 1) is set
(mid (f,1,((len f) -' (k2 -' k1)))) . j1 is set
D is non empty set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k2,((k2 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(1 -' 1) + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,1,((1 -' 1) + (len f))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(n -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,n,((n -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
0 - 1 is non empty V11() ext-real non positive negative V15() set
(len CR) -' 0 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len CR) -' 0) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
0 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (0 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (0 -' 1)) | (((len CR) -' 0) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len CR) -' 0) + 1) is non empty V33() V40(((len CR) -' 0) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len CR) -' 0) + 1 ) } is set
(f /^ (0 -' 1)) | (Seg (((len CR) -' 0) + 1)) is Relation-like FinSubsequence-like set
(len CR) - 0 is V11() ext-real non negative V15() set
(len CR) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
f | ((len CR) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len CR) + 1) is non empty V33() V40((len CR) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (len CR) + 1 ) } is set
f | (Seg ((len CR) + 1)) is Relation-like FinSubsequence-like set
dom (f | (Seg ((len CR) + 1))) is set
dom f is Element of K6(NAT)
(dom f) /\ (Seg ((len CR) + 1)) is Element of K6(NAT)
Seg (len f) is V33() V40( len f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
(Seg (len f)) /\ (Seg ((len CR) + 1)) is Element of K6(NAT)
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D is non empty set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (CR,1,(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len f) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ (1 -' 1)) | (((len f) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len f) -' 1) + 1) is non empty V33() V40(((len f) -' 1) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len f) -' 1) + 1 ) } is set
(CR /^ (1 -' 1)) | (Seg (((len f) -' 1) + 1)) is Relation-like FinSubsequence-like set
(CR /^ (1 -' 1)) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len f) is V33() V40( len f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
(CR /^ (1 -' 1)) | (Seg (len f)) is Relation-like FinSubsequence-like set
CR /^ 0 is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ 0) | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(CR /^ 0) | (Seg (len f)) is Relation-like FinSubsequence-like set
CR | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR | (Seg (len f)) is Relation-like FinSubsequence-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
CR | (len f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len f) is V33() V40( len f) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
CR | (Seg (len f)) is Relation-like FinSubsequence-like set
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR . 1 is set
f . 1 is set
mid (f,1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
D is non empty set
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Rev CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
Rev f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
Rev CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Rev f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (Rev f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,(((len f) + 1) -' (len CR)),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Rev CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Rev f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (Rev f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid ((Rev f),1,(len (Rev CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
mid ((Rev f),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) - 1 is V11() ext-real V15() set
(len f) - (len CR) is V11() ext-real V15() set
((len f) + 1) - (len CR) is V11() ext-real V15() set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
Rev (Rev CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Rev (Rev f) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(len f) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len CR)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len f) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
mid ((Rev (Rev f)),(((len f) -' (len CR)) + 1),(((len f) -' 1) + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
mid (f,(((len f) -' (len CR)) + 1),(((len f) -' 1) + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((len f) - (len CR)) + 1 is V11() ext-real V15() set
((len f) - 1) + 1 is V11() ext-real V15() set
D is non empty set
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,(((len f) + 1) -' (len CR)),(len f)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Rev f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len CR) - 1 is V11() ext-real V15() set
((len f) + 1) - (len CR) is V11() ext-real V15() set
(len f) - ((len CR) - 1) is V11() ext-real V15() set
(len f) + 0 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + ((len CR) - 1) is V11() ext-real V15() set
(len f) -' (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (len f)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len f) - (len f) is V11() ext-real V15() set
((len f) - (len f)) + 1 is V11() ext-real V15() set
(len f) - (((len f) + 1) -' (len CR)) is V11() ext-real V15() set
(len f) - (((len f) + 1) - (len CR)) is V11() ext-real V15() set
(len f) -' (((len f) + 1) -' (len CR)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) -' (((len f) + 1) -' (len CR))) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) - (((len f) + 1) -' (len CR))) + 1 is V11() ext-real V15() set
Rev CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
mid ((Rev f),(((len f) -' (len f)) + 1),(((len f) -' (((len f) + 1) -' (len CR))) + 1)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (Rev CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid ((Rev f),1,(len (Rev CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,1,((1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
0 + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,1,(0 + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((k1 -' 1) + (len CR)) -' k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((k1 -' 1) + (len CR)) -' k1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k1 -' 1)) | ((((k1 -' 1) + (len CR)) -' k1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((k1 -' 1) + (len CR)) -' k1) + 1) is non empty V33() V40((((k1 -' 1) + (len CR)) -' k1) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((k1 -' 1) + (len CR)) -' k1) + 1 ) } is set
(f /^ (k1 -' 1)) | (Seg ((((k1 -' 1) + (len CR)) -' k1) + 1)) is Relation-like FinSubsequence-like set
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) - 1 is V11() ext-real V15() set
k1 - 1 is V11() ext-real V15() set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
len (f /^ (k1 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) - (k1 -' 1) is V11() ext-real V15() set
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() Relation-like NAT -defined D -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
len (f /^ (k1 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (f /^ (k1 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len (f /^ (k1 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
<*> D is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() Relation-like NAT -defined D -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
k1 - 1 is V11() ext-real V15() set
k1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(k1 + 1) - 1 is V11() ext-real V15() set
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(k1 -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
k1 - 1 is V11() ext-real V15() set
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
n is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 - 1 is V11() ext-real V15() set
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k1 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k1,((k1 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 - 1 is V11() ext-real V15() set
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(k2 + 1) - 1 is V11() ext-real V15() set
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (k2 -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) - (k2 -' 1) is V11() ext-real V15() set
(len f) - k2 is V11() ext-real V15() set
((len f) - k2) + 1 is V11() ext-real V15() set
(k2 -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(k2 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len CR) - 1 is V11() ext-real V15() set
- 1 is V11() ext-real non positive V15() set
(- 1) + (len CR) is V11() ext-real V15() set
((- 1) + (len CR)) + k2 is V11() ext-real V15() set
(((- 1) + (len CR)) + k2) - k2 is V11() ext-real V15() set
((k2 -' 1) + (len CR)) -' k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((k2 -' 1) + (len CR)) -' k2) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len CR) - 1) + 1 is V11() ext-real V15() set
(len CR) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len CR) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
mid ((f /^ (k2 -' 1)),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (k2 -' 1)) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (k2 -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len CR) -' 1) + 1) is non empty V33() V40(((len CR) -' 1) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len CR) -' 1) + 1 ) } is set
((f /^ (k2 -' 1)) /^ (1 -' 1)) | (Seg (((len CR) -' 1) + 1)) is Relation-like FinSubsequence-like set
(f /^ (k2 -' 1)) | ((((k2 -' 1) + (len CR)) -' k2) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((k2 -' 1) + (len CR)) -' k2) + 1) is non empty V33() V40((((k2 -' 1) + (len CR)) -' k2) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((k2 -' 1) + (len CR)) -' k2) + 1 ) } is set
(f /^ (k2 -' 1)) | (Seg ((((k2 -' 1) + (len CR)) -' k2) + 1)) is Relation-like FinSubsequence-like set
mid (f,k2,((k2 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (i -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
mid ((f /^ (i -' 1)),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
i - 1 is V11() ext-real V15() set
((- 1) + (len CR)) + i is V11() ext-real V15() set
(((- 1) + (len CR)) + i) - i is V11() ext-real V15() set
(i -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((i -' 1) + (len CR)) -' i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((i -' 1) + (len CR)) -' i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(i -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(f /^ (i -' 1)) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (i -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (i -' 1)) /^ (1 -' 1)) | (Seg (((len CR) -' 1) + 1)) is Relation-like FinSubsequence-like set
(f /^ (i -' 1)) | ((((i -' 1) + (len CR)) -' i) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((i -' 1) + (len CR)) -' i) + 1) is non empty V33() V40((((i -' 1) + (len CR)) -' i) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((i -' 1) + (len CR)) -' i) + 1 ) } is set
(f /^ (i -' 1)) | (Seg ((((i -' 1) + (len CR)) -' i) + 1)) is Relation-like FinSubsequence-like set
mid (f,i,((i -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k2,((k2 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k2,((k2 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() set
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(k2 -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
mid (f,k2,((k2 -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
i - 1 is V11() ext-real V15() set
i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(i + 1) - 1 is V11() ext-real V15() set
f /^ (i -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (i -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) - (i -' 1) is V11() ext-real V15() set
(len f) - i is V11() ext-real V15() set
((len f) - i) + 1 is V11() ext-real V15() set
(i -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(i -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len CR) - 1 is V11() ext-real V15() set
- 1 is V11() ext-real non positive V15() set
(- 1) + (len CR) is V11() ext-real V15() set
((- 1) + (len CR)) + i is V11() ext-real V15() set
(((- 1) + (len CR)) + i) - i is V11() ext-real V15() set
((i -' 1) + (len CR)) -' i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((i -' 1) + (len CR)) -' i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len CR) - 1) + 1 is V11() ext-real V15() set
(len CR) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len CR) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
mid ((f /^ (i -' 1)),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (i -' 1)) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (i -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len CR) -' 1) + 1) is non empty V33() V40(((len CR) -' 1) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len CR) -' 1) + 1 ) } is set
((f /^ (i -' 1)) /^ (1 -' 1)) | (Seg (((len CR) -' 1) + 1)) is Relation-like FinSubsequence-like set
(f /^ (i -' 1)) | ((((i -' 1) + (len CR)) -' i) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((i -' 1) + (len CR)) -' i) + 1) is non empty V33() V40((((i -' 1) + (len CR)) -' i) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((i -' 1) + (len CR)) -' i) + 1 ) } is set
(f /^ (i -' 1)) | (Seg ((((i -' 1) + (len CR)) -' i) + 1)) is Relation-like FinSubsequence-like set
mid (f,i,((i -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
j is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
mid ((f /^ (j -' 1)),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
j - 1 is V11() ext-real V15() set
((- 1) + (len CR)) + j is V11() ext-real V15() set
(((- 1) + (len CR)) + j) - j is V11() ext-real V15() set
(j -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((j -' 1) + (len CR)) -' j is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((j -' 1) + (len CR)) -' j) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(j -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(f /^ (j -' 1)) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (j -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (j -' 1)) /^ (1 -' 1)) | (Seg (((len CR) -' 1) + 1)) is Relation-like FinSubsequence-like set
(f /^ (j -' 1)) | ((((j -' 1) + (len CR)) -' j) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((j -' 1) + (len CR)) -' j) + 1) is non empty V33() V40((((j -' 1) + (len CR)) -' j) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((j -' 1) + (len CR)) -' j) + 1 ) } is set
(f /^ (j -' 1)) | (Seg ((((j -' 1) + (len CR)) -' j) + 1)) is Relation-like FinSubsequence-like set
mid (f,j,((j -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
j is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
j -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (j -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
0 + k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
max (n,1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
1 - 1 is V11() ext-real V15() set
k1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
k2 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
k2 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (k2 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(len CR) - 1 is V11() ext-real V15() set
i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (i -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
i - 1 is V11() ext-real V15() set
- 1 is V11() ext-real non positive V15() set
(- 1) + (len CR) is V11() ext-real V15() set
((- 1) + (len CR)) + i is V11() ext-real V15() set
(((- 1) + (len CR)) + i) - i is V11() ext-real V15() set
(i -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((i -' 1) + (len CR)) -' i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((i -' 1) + (len CR)) -' i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len CR) - 1) + 1 is V11() ext-real V15() set
(len CR) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len CR) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(i -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
mid ((f /^ (i -' 1)),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (i -' 1)) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (i -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len CR) -' 1) + 1) is non empty V33() V40(((len CR) -' 1) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len CR) -' 1) + 1 ) } is set
((f /^ (i -' 1)) /^ (1 -' 1)) | (Seg (((len CR) -' 1) + 1)) is Relation-like FinSubsequence-like set
(f /^ (i -' 1)) | ((((i -' 1) + (len CR)) -' i) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((i -' 1) + (len CR)) -' i) + 1) is non empty V33() V40((((i -' 1) + (len CR)) -' i) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((i -' 1) + (len CR)) -' i) + 1 ) } is set
(f /^ (i -' 1)) | (Seg ((((i -' 1) + (len CR)) -' i) + 1)) is Relation-like FinSubsequence-like set
mid (f,i,((i -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (i -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
i -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (i -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
i - 1 is V11() ext-real V15() set
- 1 is V11() ext-real non positive V15() set
(- 1) + (len CR) is V11() ext-real V15() set
((- 1) + (len CR)) + i is V11() ext-real V15() set
(((- 1) + (len CR)) + i) - i is V11() ext-real V15() set
(i -' 1) + (len CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((i -' 1) + (len CR)) -' i is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(((i -' 1) + (len CR)) -' i) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len CR) - 1) + 1 is V11() ext-real V15() set
(len CR) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len CR) -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(i -' 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
mid ((f /^ (i -' 1)),1,(len CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ (i -' 1)) /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ (i -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len CR) -' 1) + 1) is non empty V33() V40(((len CR) -' 1) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= ((len CR) -' 1) + 1 ) } is set
((f /^ (i -' 1)) /^ (1 -' 1)) | (Seg (((len CR) -' 1) + 1)) is Relation-like FinSubsequence-like set
(f /^ (i -' 1)) | ((((i -' 1) + (len CR)) -' i) + 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((((i -' 1) + (len CR)) -' i) + 1) is non empty V33() V40((((i -' 1) + (len CR)) -' i) + 1) Element of K6(NAT)
{ b₁ where b₁ is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b₁ & b₁ <= (((i -' 1) + (len CR)) -' i) + 1 ) } is set
(f /^ (i -' 1)) | (Seg ((((i -' 1) + (len CR)) -' i) + 1)) is Relation-like FinSubsequence-like set
mid (f,i,((i -' 1) + (len CR))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (f /^ (i -' 1)) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
len CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,CR) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,CR) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR /^ (len (D,f,CR)) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,(CR /^ (len (D,f,CR)))) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
len f is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
(len f) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
((len f) + 1) -' (len f) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
((len f) + 1) - (len f) is V11() ext-real V15() set
1 -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V15() V33() V38() Element of NAT
(0 + 1) -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (1 -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
CR is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
CR -' 1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT
f /^ (CR -' 1) is Relation-like NAT -defined D -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,f,1) is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT