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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= 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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= (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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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)
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real non negative V15() V33() V38() Element of NAT : ( 1 <= b1 & b1 <= ((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() V1