REAL is set
NAT is non empty V24() V25() V26() Element of K19(REAL)
K19(REAL) is set
NAT is non empty V24() V25() V26() set
K19(NAT) is set
K19(NAT) is set
COMPLEX is set
1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like Element of NAT
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
i -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (i -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (i -' 1) is V34() V41(i -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= i -' 1 ) } is set
f | (Seg (i -' 1)) is Relation-like NAT -defined Seg (i -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
f . i is set
<*(f . i)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(f . i)] is set
{[1,(f . i)]} is Relation-like Function-like non empty set
(f | (i -' 1)) ^ <*(f . i)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
f /^ i is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
k -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' i) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ i) | ((k -' i) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((k -' i) -' 1) is V34() V41((k -' i) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (k -' i) -' 1 ) } is set
(f /^ i) | (Seg ((k -' i) -' 1)) is Relation-like NAT -defined Seg ((k -' i) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((k -' i) -' 1)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
f . k is set
<*(f . k)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(f . k)] is set
{[1,(f . k)]} is Relation-like Function-like non empty set
(((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((k -' i) -' 1))) ^ <*(f . k)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
f /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((k -' i) -' 1))) ^ <*(f . k)*>) ^ (f /^ k) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
dom f is Element of K19(NAT)
i -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
((k -' i) -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len f) -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f /^ i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
F is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | F is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg F is V34() V41(F) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= F ) } is set
f | (Seg F) is Relation-like NAT -defined Seg F -defined NAT -defined D -valued Function-like FinSubsequence-like set
len (f | F) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /^ l is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
dom (f /^ l) is Element of K19(NAT)
(((k -' i) -' 1) + 1) + l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ l) /. (((k -' i) -' 1) + 1) is Element of D
f /. F is Element of D
f /^ F is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | F) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | F) ^ (f /^ F)) /^ l is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | F) /^ l is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | F) /^ l) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ l) | (((k -' i) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((k -' i) -' 1) + 1) is non empty V34() V41(((k -' i) -' 1) + 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= ((k -' i) -' 1) + 1 ) } is set
(f /^ l) | (Seg (((k -' i) -' 1) + 1)) is Relation-like NAT -defined Seg (((k -' i) -' 1) + 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f /^ l) | (((k -' i) -' 1) + 1)) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ l) | ((k -' i) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ l) | (Seg ((k -' i) -' 1)) is Relation-like NAT -defined Seg ((k -' i) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*((f /^ l) /. (((k -' i) -' 1) + 1))*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,((f /^ l) /. (((k -' i) -' 1) + 1))] is set
{[1,((f /^ l) /. (((k -' i) -' 1) + 1))]} is Relation-like Function-like non empty set
((f /^ l) | ((k -' i) -' 1)) ^ <*((f /^ l) /. (((k -' i) -' 1) + 1))*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f /^ l) | ((k -' i) -' 1)) ^ <*((f /^ l) /. (((k -' i) -' 1) + 1))*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f . F is set
<*(f . F)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(f . F)] is set
{[1,(f . F)]} is Relation-like Function-like non empty set
((f /^ l) | ((k -' i) -' 1)) ^ <*(f . F)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f /^ l) | ((k -' i) -' 1)) ^ <*(f . F)*>) ^ (f /^ F) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
l -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (l -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (l -' 1) is V34() V41(l -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= l -' 1 ) } is set
f | (Seg (l -' 1)) is Relation-like NAT -defined Seg (l -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
f . l is set
<*(f . l)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(f . l)] is set
{[1,(f . l)]} is Relation-like Function-like non empty set
(f | (l -' 1)) ^ <*(f . l)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((f | (l -' 1)) ^ <*(f . l)*>) ^ (f /^ l) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
<*(f . F)*> ^ (f /^ F) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((f /^ l) | ((k -' i) -' 1)) ^ (<*(f . F)*> ^ (f /^ F)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((f | (l -' 1)) ^ <*(f . l)*>) ^ (((f /^ l) | ((k -' i) -' 1)) ^ (<*(f . F)*> ^ (f /^ F))) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1))) ^ (<*(f . F)*> ^ (f /^ F)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1))) ^ <*(f . F)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1))) ^ <*(f . F)*>) ^ (f /^ F) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
D is ext-real V24() V25() V26() V30() V31() V32() V33() set
i is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len i is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
i ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len (i ^ f) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(i ^ f) . D is set
k ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(k ^ f) . D is set
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len i) + (len f) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D - (len i) is ext-real V31() V32() V33() set
((len i) + (len f)) - (len i) is ext-real V31() V32() V33() set
(len i) - (len i) is ext-real V31() V32() V33() set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom f is Element of K19(NAT)
l + (len i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(i ^ f) . (l + (len i)) is set
f . l is set
(len k) + l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k ^ f) . ((len k) + l) is set
D is ext-real V24() V25() V26() V30() V31() V32() V33() set
f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f . D is set
i is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
i ^ f is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len i is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len i) + D is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(i ^ f) . ((len i) + D) is set
dom f is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
f /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
dom (f /^ k) is Element of K19(NAT)
(f /^ k) . i is set
k + i is ext-real V31() V32() V33() set
f . (k + i) is set
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
l + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom f is Element of K19(NAT)
f /^ l is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ l) /. j is Element of D
f /. (l + j) is Element of D
(f /^ l) . j is set
D is ext-real V24() V25() V26() V30() V31() V32() V33() set
D -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f is ext-real V24() V25() V26() V30() V31() V32() V33() set
D -' f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D -' f) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D -' 1) -' f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D -' (f + 1) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set
D is non empty set
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is Element of D
f +* (i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like set
i -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (i -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (i -' 1) is V34() V41(i -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= i -' 1 ) } is set
f | (Seg (i -' 1)) is Relation-like NAT -defined Seg (i -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
(f | (i -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ i is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (i -' 1)) ^ <*k*>) ^ (f /^ i) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
dom f is Element of K19(NAT)
dom f is Element of K19(NAT)
j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
l is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f +* (j,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
i is Element of D
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,k,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
i is Element of D
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,f,k,i) is set
rng f is set
{i} is non empty set
(rng f) \/ {i} is non empty set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,f,k,i) is set
dom f is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,i) . k is set
dom f is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,i) /. k is Element of D
dom f is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(len f) - k is ext-real V31() V32() V33() set
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k - 1 is ext-real V31() V32() V33() set
k -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (k -' 1) is V34() V41(k -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= k -' 1 ) } is set
f | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
(f | (k -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
len ((f | (k -' 1)) ^ <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f | (k -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (k -' 1))) + (len <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' 1) + (len <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
k + j is ext-real V31() V32() V33() set
(D,f,k,i) . (k + j) is set
(f /^ k) . j is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,k,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
((f | (k -' 1)) ^ <*i*>) ^ (f /^ k) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
len (((f | (k -' 1)) ^ <*i*>) ^ (f /^ k)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f /^ k) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
k + (len (f /^ k)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom (f /^ k) is Element of K19(NAT)
(len ((f | (k -' 1)) ^ <*i*>)) + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(((f | (k -' 1)) ^ <*i*>) ^ (f /^ k)) . ((len ((f | (k -' 1)) ^ <*i*>)) + j) is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
f /. k is Element of D
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) /. k is Element of D
F is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom f is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
k is Element of D
<*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
j -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (j -' 1) is V34() V41(j -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= j -' 1 ) } is set
f | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(f | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
l is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,l,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,l,i),j,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
l -' j is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(l -' j) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ j) | ((l -' j) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((l -' j) -' 1) is V34() V41((l -' j) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (l -' j) -' 1 ) } is set
(f /^ j) | (Seg ((l -' j) -' 1)) is Relation-like NAT -defined Seg ((l -' j) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' j) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' j) -' 1))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ l is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' j) -' 1))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
l -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (l -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (l -' 1) is V34() V41(l -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= l -' 1 ) } is set
f | (Seg (l -' 1)) is Relation-like NAT -defined Seg (l -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
1 + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f | (l -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f | (l -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
len ((f | (l -' 1)) ^ <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (l -' 1))) + (len <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (l -' 1))) + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(l -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,l,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,l,i) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,l,i) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((D,f,l,i) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,l,i) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((D,f,l,i) /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) ^ <*i*>) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) ^ <*i*>) /^ j) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f | (l -' 1)) ^ <*i*>) /^ j) ^ (f /^ l)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (l -' 1)) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) /^ j) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) /^ j) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f | (l -' 1)) /^ j) ^ <*i*>) ^ (f /^ l)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(l -' 1) -' j is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ j) | ((l -' 1) -' j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((l -' 1) -' j) is V34() V41((l -' 1) -' j) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (l -' 1) -' j ) } is set
(f /^ j) | (Seg ((l -' 1) -' j)) is Relation-like NAT -defined Seg ((l -' 1) -' j) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f /^ j) | ((l -' 1) -' j)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f /^ j) | ((l -' 1) -' j)) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f /^ j) | ((l -' 1) -' j)) ^ <*i*>) ^ (f /^ l)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ (((f /^ j) | ((l -' 1) -' j)) ^ <*i*>) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ (((f /^ j) | ((l -' 1) -' j)) ^ <*i*>)) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) ^ <*i*>) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) ^ <*i*>) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (l -' 1)) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (l -' 1)) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (l -' 1)) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (l -' 1)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((f | (l -' 1)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
<*f*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
i is Element of D
(D,<*f*>,1,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
1 - 1 is ext-real V31() V32() V33() set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like FinSequence of D
<*f*> ^ (<*> D) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ (<*> D)) /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len <*f*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*f*> | (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (1 -' 1) is V34() V41(1 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 -' 1 ) } is set
<*f*> | (Seg (1 -' 1)) is Relation-like NAT -defined Seg (1 -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(<*f*> | (1 -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f*> | (1 -' 1)) ^ <*i*>) ^ (<*f*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f*> | 0 is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like FinSequence of D
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
<*f*> | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like set
(<*f*> | 0) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f*> | 0) ^ <*i*>) ^ (<*f*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ (<*f*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
j /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ (j /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
<*f,i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is Element of D
(D,<*f,i*>,1,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k,i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
<*k*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
len <*f,i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i*> is non empty Element of K19(NAT)
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*f,i*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i*> /. 2 is Element of D
<*(<*f,i*> /. 2)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(<*f,i*> /. 2)] is set
{[1,(<*f,i*> /. 2)]} is Relation-like Function-like non empty set
<*f,i*> . 2 is set
<*(<*f,i*> . 2)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i*> . 2)] is set
{[1,(<*f,i*> . 2)]} is Relation-like Function-like non empty set
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*f,i*> | (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (1 -' 1) is V34() V41(1 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 -' 1 ) } is set
<*f,i*> | (Seg (1 -' 1)) is Relation-like NAT -defined Seg (1 -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
(<*f,i*> | (1 -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i*> | (1 -' 1)) ^ <*k*>) ^ (<*f,i*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i*> | 0 is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like FinSequence of D
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
<*f,i*> | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like set
(<*f,i*> | 0) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i*> | 0) ^ <*k*>) ^ (<*f,i*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
{} ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
({} ^ <*k*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
<*k*> ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
<*f,i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is Element of D
(D,<*f,i*>,2,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
<*f*> ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
2 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(1 + 1) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*f,i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i*> is non empty Element of K19(NAT)
<*f,i*> | (2 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (2 -' 1) is V34() V41(2 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 2 -' 1 ) } is set
<*f,i*> | (Seg (2 -' 1)) is Relation-like NAT -defined Seg (2 -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
(<*f,i*> | (2 -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i*> /^ 2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i*> | (2 -' 1)) ^ <*k*>) ^ (<*f,i*> /^ 2) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i*> | 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg 1 is non empty V34() V41(1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
<*f,i*> | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined D -valued Function-like FinSubsequence-like set
(<*f,i*> | 1) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i*> /^ (len <*f,i*>) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i*> | 1) ^ <*k*>) ^ (<*f,i*> /^ (len <*f,i*>)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i*> | 1) ^ <*k*>) ^ {} is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
<*f,i*> /. 1 is Element of D
<*(<*f,i*> /. 1)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(<*f,i*> /. 1)] is set
{[1,(<*f,i*> /. 1)]} is Relation-like Function-like non empty set
<*(<*f,i*> /. 1)*> ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D
(<*(<*f,i*> /. 1)*> ^ <*k*>) ^ {} is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
<*f,i*> . 1 is set
<*(<*f,i*> . 1)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i*> . 1)] is set
{[1,(<*f,i*> . 1)]} is Relation-like Function-like non empty set
<*(<*f,i*> . 1)*> ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
<*f*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
k is Element of D
<*f,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
(<*f*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is Element of D
(D,<*f,i,k*>,1,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*j,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*j*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,j] is set
{[1,j]} is Relation-like Function-like non empty set
<*j*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*j*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*f,i,k*> | (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (1 -' 1) is V34() V41(1 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 -' 1 ) } is set
<*f,i,k*> | (Seg (1 -' 1)) is Relation-like NAT -defined Seg (1 -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
(<*f,i,k*> | (1 -' 1)) ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i,k*> | (1 -' 1)) ^ <*j*>) ^ (<*f,i,k*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> | 0 is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like FinSequence of D
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
<*f,i,k*> | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like set
(<*f,i,k*> | 0) ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i,k*> | 0) ^ <*j*>) ^ (<*f,i,k*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*j*> ^ (<*f,i,k*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
<*j*> ^ <*i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 2) FinSequence-like FinSubsequence-like FinSequence of D
1 + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
<*j*> ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D
<*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
(<*j*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
k is Element of D
<*f,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
(<*f*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is Element of D
(D,<*f,i,k*>,2,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,j,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*j*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,j] is set
{[1,j]} is Relation-like Function-like non empty set
<*f*> ^ <*j*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*f*> ^ <*j*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
2 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(1 + 1) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i,k*> is non empty Element of K19(NAT)
<*f,i,k*> | (2 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (2 -' 1) is V34() V41(2 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 2 -' 1 ) } is set
<*f,i,k*> | (Seg (2 -' 1)) is Relation-like NAT -defined Seg (2 -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
(<*f,i,k*> | (2 -' 1)) ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> /^ 2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i,k*> | (2 -' 1)) ^ <*j*>) ^ (<*f,i,k*> /^ 2) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> | 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg 1 is non empty V34() V41(1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
<*f,i,k*> | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined D -valued Function-like FinSubsequence-like set
(<*f,i,k*> | 1) ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> /. 3 is Element of D
<*(<*f,i,k*> /. 3)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(<*f,i,k*> /. 3)] is set
{[1,(<*f,i,k*> /. 3)]} is Relation-like Function-like non empty set
((<*f,i,k*> | 1) ^ <*j*>) ^ <*(<*f,i,k*> /. 3)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> . 3 is set
<*(<*f,i,k*> . 3)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i,k*> . 3)] is set
{[1,(<*f,i,k*> . 3)]} is Relation-like Function-like non empty set
((<*f,i,k*> | 1) ^ <*j*>) ^ <*(<*f,i,k*> . 3)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
<*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i,k*> | 1) ^ <*j*>) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> /. 1 is Element of D
<*(<*f,i,k*> /. 1)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(<*f,i,k*> /. 1)] is set
{[1,(<*f,i,k*> /. 1)]} is Relation-like Function-like non empty set
<*(<*f,i,k*> /. 1)*> ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D
(<*(<*f,i,k*> /. 1)*> ^ <*j*>) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> . 1 is set
<*(<*f,i,k*> . 1)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i,k*> . 1)] is set
{[1,(<*f,i,k*> . 1)]} is Relation-like Function-like non empty set
<*(<*f,i,k*> . 1)*> ^ <*j*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*(<*f,i,k*> . 1)*> ^ <*j*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*f*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ <*j*>) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
k is Element of D
<*f,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
(<*f*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is Element of D
(D,<*f,i,k*>,3,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*j*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,j] is set
{[1,j]} is Relation-like Function-like non empty set
(<*f*> ^ <*i*>) ^ <*j*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
3 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(2 + 1) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i,k*> is non empty Element of K19(NAT)
<*f,i,k*> | (3 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (3 -' 1) is V34() V41(3 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 3 -' 1 ) } is set
<*f,i,k*> | (Seg (3 -' 1)) is Relation-like NAT -defined Seg (3 -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
(<*f,i,k*> | (3 -' 1)) ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> /^ 3 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i,k*> | (3 -' 1)) ^ <*j*>) ^ (<*f,i,k*> /^ 3) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> | 2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg 2 is non empty V34() V41(2) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
<*f,i,k*> | (Seg 2) is Relation-like NAT -defined Seg 2 -defined NAT -defined D -valued Function-like FinSubsequence-like set
(<*f,i,k*> | 2) ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> /^ (len <*f,i,k*>) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i,k*> | 2) ^ <*j*>) ^ (<*f,i,k*> /^ (len <*f,i,k*>)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*f,i,k*> | 2) ^ <*j*>) ^ {} is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
<*f,i,k*> /. 1 is Element of D
<*f,i,k*> /. 2 is Element of D
<*(<*f,i,k*> /. 1),(<*f,i,k*> /. 2)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*(<*f,i,k*> /. 1)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i,k*> /. 1)] is set
{[1,(<*f,i,k*> /. 1)]} is Relation-like Function-like non empty set
<*(<*f,i,k*> /. 2)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i,k*> /. 2)] is set
{[1,(<*f,i,k*> /. 2)]} is Relation-like Function-like non empty set
<*(<*f,i,k*> /. 1)*> ^ <*(<*f,i,k*> /. 2)*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
<*(<*f,i,k*> /. 1),(<*f,i,k*> /. 2)*> ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2 + 1) FinSequence-like FinSubsequence-like FinSequence of D
2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*f,i,k*> . 1 is set
<*(<*f,i,k*> . 1)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i,k*> . 1)] is set
{[1,(<*f,i,k*> . 1)]} is Relation-like Function-like non empty set
<*(<*f,i,k*> /. 2)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
<*(<*f,i,k*> . 1)*> ^ <*(<*f,i,k*> /. 2)*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*(<*f,i,k*> . 1)*> ^ <*(<*f,i,k*> /. 2)*>) ^ <*j*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*f,i,k*> . 2 is set
<*(<*f,i,k*> . 2)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(<*f,i,k*> . 2)] is set
{[1,(<*f,i,k*> . 2)]} is Relation-like Function-like non empty set
<*(<*f,i,k*> . 1)*> ^ <*(<*f,i,k*> . 2)*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*(<*f,i,k*> . 1)*> ^ <*(<*f,i,k*> . 2)*>) ^ <*j*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*f*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*(<*f,i,k*> . 2)*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*f*> ^ <*(<*f,i,k*> . 2)*>) ^ <*j*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ <*i*>) ^ <*j*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of D
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
f is ext-real V24() V25() V26() V30() V31() V32() V33() set
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
Swap (D,f,i) is Relation-like Function-like set
dom (Swap (D,f,i)) is set
dom D is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
Swap (f,i,k) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng (Swap (f,i,k)) is set
rng f is set
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /. k is Element of D
(D,f,i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. i is Element of D
(D,(D,f,i,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
dom f is Element of K19(NAT)
f . k is set
f . i is set
dom f is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,i,k) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom (D,f,i,k) is Element of K19(NAT)
dom f is Element of K19(NAT)
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
f . i is set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,k) . i is set
f . k is set
(D,f,i,k) . k is set
dom f is Element of K19(NAT)
f /. k is Element of D
(D,f,i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,i,(f /. k)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /. i is Element of D
(D,(D,f,i,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),k,(f /. i)) . i is set
f /. i is Element of D
(D,(D,f,i,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),k,(f /. i)) . k is set
(D,(D,f,i,(f /. k)),k,(f /. i)) . i is set
(D,f,i,(f /. k)) . i is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,k,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. k is Element of D
(D,f,k,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. k)),k,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,k),k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,i,k) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
f . j is set
(D,(D,f,i,k),k,i) . j is set
(D,f,j,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,k) . k is set
(D,f,i,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,j) . i is set
(D,f,i,k) /. i is Element of D
(D,(D,f,i,k),k,((D,f,i,k) /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,k) /. k is Element of D
(D,(D,(D,f,i,k),k,((D,f,i,k) /. i)),i,((D,f,i,k) /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,i,k),k,((D,f,i,k) /. i)),i,((D,f,i,k) /. k)) . j is set
(D,(D,f,i,k),k,((D,f,i,k) /. i)) . j is set
(D,f,i,k) . j is set
f /. k is Element of D
(D,f,i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. i is Element of D
(D,(D,f,i,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),k,(f /. i)) . j is set
(D,f,i,(f /. k)) . j is set
len (D,(D,f,i,k),k,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,i,k) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /. i is Element of D
(D,f,k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. k is Element of D
(D,f,i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,i,k) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,k,(f /. i)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,i,(f /. k)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
F is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) . F is set
(D,f,k,i) . F is set
(D,f,i,F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,F) . F is set
(D,(D,f,i,(f /. k)),F,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),F,(f /. i)) . F is set
(D,(D,f,k,(f /. i)),F,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. i)),F,(f /. i)) . F is set
(D,f,F,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,F,i) . F is set
(D,(D,f,i,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),k,(f /. i)) . F is set
(D,f,F,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,F,(f /. k)) . F is set
(D,(D,f,k,(f /. i)),F,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. i)),F,(f /. k)) . F is set
(D,(D,f,i,(f /. k)),F,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),F,(f /. i)) . F is set
(D,f,k,(f /. i)) . F is set
(D,(D,f,k,(f /. i)),i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. i)),i,(f /. k)) . F is set
(D,(D,f,i,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),k,(f /. i)) . F is set
(D,f,i,(f /. k)) . F is set
f . F is set
(D,f,k,(f /. i)) . F is set
(D,(D,f,k,(f /. i)),i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. i)),i,(f /. k)) . F is set
len (D,f,k,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,f,i,k) is set
rng f is set
D is non empty set
f is Element of D
i is Element of D
<*f,i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,<*f,i*>,1,2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i,f*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ <*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
len <*f,i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i*> is non empty Element of K19(NAT)
<*f,i*> /. 1 is Element of D
<*f,i*> . 1 is set
<*f,i*> /. 2 is Element of D
<*f,i*> . 2 is set
(D,<*f,i*>,1,(<*f,i*> /. 2)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,<*f,i*>,1,(<*f,i*> /. 2)),2,(<*f,i*> /. 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i,i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(D,<*i,i*>,2,(<*f,i*> /. 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
k is Element of D
<*f,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
(<*f*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,<*f,i,k*>,1,2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i,f,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ <*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*i*> ^ <*f*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i,k*> is non empty Element of K19(NAT)
<*f,i,k*> /. 1 is Element of D
<*f,i,k*> . 1 is set
<*f,i,k*> /. 2 is Element of D
<*f,i,k*> . 2 is set
(D,<*f,i,k*>,1,(<*f,i,k*> /. 2)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,<*f,i,k*>,1,(<*f,i,k*> /. 2)),2,(<*f,i,k*> /. 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*i*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(D,<*i,i,k*>,2,(<*f,i,k*> /. 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
k is Element of D
<*f,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
(<*f*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,<*f,i,k*>,1,3) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k,i,f*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*k*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*k*> ^ <*i*>) ^ <*f*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i,k*> is non empty Element of K19(NAT)
<*f,i,k*> /. 1 is Element of D
<*f,i,k*> . 1 is set
<*f,i,k*> /. 3 is Element of D
<*f,i,k*> . 3 is set
(D,<*f,i,k*>,1,(<*f,i,k*> /. 3)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,<*f,i,k*>,1,(<*f,i,k*> /. 3)),3,(<*f,i,k*> /. 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*k,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
(<*k*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(D,<*k,i,k*>,3,(<*f,i,k*> /. 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D
i is Element of D
k is Element of D
<*f,i,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is Relation-like Function-like non empty set
<*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
<*f*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{[1,k]} is Relation-like Function-like non empty set
(<*f*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,<*f,i,k*>,2,3) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k,i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
<*f*> ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*f*> ^ <*k*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i,k*> is non empty Element of K19(NAT)
<*f,i,k*> /. 2 is Element of D
<*f,i,k*> . 2 is set
<*f,i,k*> /. 3 is Element of D
<*f,i,k*> . 3 is set
(D,<*f,i,k*>,2,(<*f,i,k*> /. 3)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,<*f,i,k*>,2,(<*f,i,k*> /. 3)),3,(<*f,i,k*> /. 2)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,k,k*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(3) FinSequence-like FinSubsequence-like FinSequence of D
(<*f*> ^ <*k*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty V34() V41((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(D,<*f,k,k*>,3,(<*f,i,k*> /. 2)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
i -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (i -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (i -' 1) is V34() V41(i -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= i -' 1 ) } is set
f | (Seg (i -' 1)) is Relation-like NAT -defined Seg (i -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
f /^ i is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. i is Element of D
<*(f /. i)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. i)] is set
{[1,(f /. i)]} is Relation-like Function-like non empty set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. k is Element of D
<*(f /. k)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. k)] is set
{[1,(f /. k)]} is Relation-like Function-like non empty set
(f | (i -' 1)) ^ <*(f /. k)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
k -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' i) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ i) | ((k -' i) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((k -' i) -' 1) is V34() V41((k -' i) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (k -' i) -' 1 ) } is set
(f /^ i) | (Seg ((k -' i) -' 1)) is Relation-like NAT -defined Seg ((k -' i) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (i -' 1)) ^ <*(f /. k)*>) ^ ((f /^ i) | ((k -' i) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (i -' 1)) ^ <*(f /. k)*>) ^ ((f /^ i) | ((k -' i) -' 1))) ^ <*(f /. i)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (i -' 1)) ^ <*(f /. k)*>) ^ ((f /^ i) | ((k -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ k) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. i)),i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. 1 is Element of D
<*(f /. 1)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. 1)] is set
{[1,(f /. 1)]} is Relation-like Function-like non empty set
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,1,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. i is Element of D
<*(f /. i)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. i)] is set
{[1,(f /. i)]} is Relation-like Function-like non empty set
i -' 2 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ 1) | (i -' 2) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (i -' 2) is V34() V41(i -' 2) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= i -' 2 ) } is set
(f /^ 1) | (Seg (i -' 2)) is Relation-like NAT -defined Seg (i -' 2) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*(f /. i)*> ^ ((f /^ 1) | (i -' 2)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ i is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (1 -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (1 -' 1) is V34() V41(1 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 -' 1 ) } is set
f | (Seg (1 -' 1)) is Relation-like NAT -defined Seg (1 -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(f | (1 -' 1)) ^ <*(f /. i)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
i -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(i -' 1) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ 1) | ((i -' 1) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((i -' 1) -' 1) is V34() V41((i -' 1) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (i -' 1) -' 1 ) } is set
(f /^ 1) | (Seg ((i -' 1) -' 1)) is Relation-like NAT -defined Seg ((i -' 1) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (1 -' 1)) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (1 -' 1)) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (1 -' 1)) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f | 0 is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like FinSequence of D
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() V41( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
f | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered V46() FuncSeq-like set
(f | 0) ^ <*(f /. i)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | 0) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | 0) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | 0) ^ <*(f /. i)*>) ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. i)*> ^ ((f /^ 1) | ((i -' 1) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*(f /. i)*> ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((<*(f /. i)*> ^ ((f /^ 1) | ((i -' 1) -' 1))) ^ <*(f /. 1)*>) ^ (f /^ i) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /. (len f) is Element of D
<*(f /. (len f))*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. (len f))] is set
{[1,(f /. (len f))]} is Relation-like Function-like non empty set
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,(len f)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (i -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (i -' 1) is V34() V41(i -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= i -' 1 ) } is set
f | (Seg (i -' 1)) is Relation-like NAT -defined Seg (i -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(f | (i -' 1)) ^ <*(f /. (len f))*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(len f) -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
((len f) -' i) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /^ i is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ i) | (((len f) -' i) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((len f) -' i) -' 1) is V34() V41(((len f) -' i) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= ((len f) -' i) -' 1 ) } is set
(f /^ i) | (Seg (((len f) -' i) -' 1)) is Relation-like NAT -defined Seg (((len f) -' i) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. i is Element of D
<*(f /. i)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. i)] is set
{[1,(f /. i)]} is Relation-like Function-like non empty set
(((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ (len f) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ (len f)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>) ^ {} is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
f . k is set
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,j) . k is set
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /. j is Element of D
(D,f,i,(f /. j)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. i is Element of D
(D,(D,f,i,(f /. j)),j,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. j)),j,(f /. i)) . k is set
(D,f,i,(f /. j)) . k is set
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
f /. k is Element of D
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,j) /. k is Element of D
dom f is Element of K19(NAT)
len (D,f,i,j) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom (D,f,i,j) is Element of K19(NAT)
(D,f,i,j) . k is set
f . k is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
f /. i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,k) /. i is Element of D
f /. k is Element of D
(D,f,i,k) /. k is Element of D
dom f is Element of K19(NAT)
len (D,f,i,k) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom (D,f,i,k) is Element of K19(NAT)
(D,f,i,k) . k is set
f . i is set
(D,f,i,k) . i is set
f . k is set
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,k,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,j),k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,j,i),k,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
dom f is Element of K19(NAT)
(D,f,k,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. j is Element of D
<*(f /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. j)] is set
{[1,(f /. j)]} is Relation-like Function-like non empty set
k -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (k -' 1) is V34() V41(k -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= k -' 1 ) } is set
f | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(f | (k -' 1)) ^ <*(f /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
j -' k is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(j -' k) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ k) | ((j -' k) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((j -' k) -' 1) is V34() V41((j -' k) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (j -' k) -' 1 ) } is set
(f /^ k) | (Seg ((j -' k) -' 1)) is Relation-like NAT -defined Seg ((j -' k) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (k -' 1)) ^ <*(f /. j)*>) ^ ((f /^ k) | ((j -' k) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. k is Element of D
<*(f /. k)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. k)] is set
{[1,(f /. k)]} is Relation-like Function-like non empty set
(((f | (k -' 1)) ^ <*(f /. j)*>) ^ ((f /^ k) | ((j -' k) -' 1))) ^ <*(f /. k)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (k -' 1)) ^ <*(f /. j)*>) ^ ((f /^ k) | ((j -' k) -' 1))) ^ <*(f /. k)*>) ^ (f /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. k)*> ^ (f /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (k -' 1)) ^ <*(f /. j)*>) ^ ((f /^ k) | ((j -' k) -' 1))) ^ (<*(f /. k)*> ^ (f /^ j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (k -' 1)) ^ <*(f /. j)*>) ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,j,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom (D,f,j,i) is Element of K19(NAT)
f . k is set
(D,f,j,i) . k is set
(D,f,j,i) /. k is Element of D
j -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (j -' 1) is V34() V41(j -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= j -' 1 ) } is set
f | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
len (f | (j -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
len (D,f,k,j) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len ((f | (k -' 1)) ^ <*(f /. j)*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f | (k -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*(f /. j)*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (k -' 1))) + (len <*(f /. j)*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (k -' 1))) + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,k,j) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,j) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((D,f,k,j) | (k -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,j) /^ (len ((f | (k -' 1)) ^ <*(f /. j)*>)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,k,j) | (k -' 1)) ^ <*i*>) ^ ((D,f,k,j) /^ (len ((f | (k -' 1)) ^ <*(f /. j)*>))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,k,j) | (k -' 1)) ^ <*i*>) ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j)))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (k -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (k -' 1)) ^ <*i*>) ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (len (f | (k -' 1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len (f | (k -' 1))) is V34() V41( len (f | (k -' 1))) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= len (f | (k -' 1)) ) } is set
((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (Seg (len (f | (k -' 1)))) is Relation-like NAT -defined Seg (len (f | (k -' 1))) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (len (f | (k -' 1)))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (k -' 1)) ^ (<*(f /. j)*> ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))))) | (len (f | (k -' 1)))) ^ <*i*>) ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (k -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (k -' 1)) ^ <*i*>) ^ (((f /^ k) | ((j -' k) -' 1)) ^ (<*(f /. k)*> ^ (f /^ j))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
len ((f | (j -' 1)) ^ <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (j -' 1))) + (len <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (j -' 1))) + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(j -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,j,i) /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((D,f,j,i) /^ k) | ((j -' k) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((D,f,j,i) /^ k) | (Seg ((j -' k) -' 1)) is Relation-like NAT -defined Seg ((j -' k) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
k + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
j -' (k + 1) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
((D,f,j,i) /^ k) | (j -' (k + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (j -' (k + 1)) is V34() V41(j -' (k + 1)) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= j -' (k + 1) ) } is set
((D,f,j,i) /^ k) | (Seg (j -' (k + 1))) is Relation-like NAT -defined Seg (j -' (k + 1)) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(j -' 1) -' k is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
((D,f,j,i) /^ k) | ((j -' 1) -' k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((j -' 1) -' k) is V34() V41((j -' 1) -' k) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (j -' 1) -' k ) } is set
((D,f,j,i) /^ k) | (Seg ((j -' 1) -' k)) is Relation-like NAT -defined Seg ((j -' 1) -' k) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,f,j,i) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((D,f,j,i) | (j -' 1)) /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ <*i*>) ^ (f /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (j -' 1)) /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i*> ^ (f /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ (<*i*> ^ (f /^ j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (j -' 1)) /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (len (f | (j -' 1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len (f | (j -' 1))) is V34() V41( len (f | (j -' 1))) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= len (f | (j -' 1)) ) } is set
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (Seg (len (f | (j -' 1)))) is Relation-like NAT -defined Seg (len (f | (j -' 1))) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (len (f | (j -' 1)))) /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ k) | ((j -' 1) -' k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ k) | (Seg ((j -' 1) -' k)) is Relation-like NAT -defined Seg ((j -' 1) -' k) -defined NAT -defined D -valued Function-like FinSubsequence-like set
1 + k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
j -' (1 + k) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ k) | (j -' (1 + k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (j -' (1 + k)) is V34() V41(j -' (1 + k)) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= j -' (1 + k) ) } is set
(f /^ k) | (Seg (j -' (1 + k))) is Relation-like NAT -defined Seg (j -' (1 + k)) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,f,j,i) . j is set
(D,f,j,i) /. j is Element of D
(D,f,j,i) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(f | (j -' 1)) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,f,j,i) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*((D,f,j,i) /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,((D,f,j,i) /. j)] is set
{[1,((D,f,j,i) /. j)]} is Relation-like Function-like non empty set
((D,f,j,i) | (k -' 1)) ^ <*((D,f,j,i) /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,j,i) | (k -' 1)) ^ <*((D,f,j,i) /. j)*>) ^ (((D,f,j,i) /^ k) | ((j -' k) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*((D,f,j,i) /. k)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,((D,f,j,i) /. k)] is set
{[1,((D,f,j,i) /. k)]} is Relation-like Function-like non empty set
((((D,f,j,i) | (k -' 1)) ^ <*((D,f,j,i) /. j)*>) ^ (((D,f,j,i) /^ k) | ((j -' k) -' 1))) ^ <*((D,f,j,i) /. k)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((D,f,j,i) | (k -' 1)) ^ <*((D,f,j,i) /. j)*>) ^ (((D,f,j,i) /^ k) | ((j -' k) -' 1))) ^ <*((D,f,j,i) /. k)*>) ^ ((D,f,j,i) /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (k -' 1)) ^ <*i*>) ^ ((f /^ k) | ((j -' k) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f . k)*> is Relation-like NAT -defined Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(f . k)] is set
{[1,(f . k)]} is Relation-like Function-like non empty set
<*(f . k)*> ^ (f /^ j) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f | (k -' 1)) ^ <*i*>) ^ ((f /^ k) | ((j -' k) -' 1))) ^ (<*(f . k)*> ^ (f /^ j)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f | (k -' 1)) ^ <*i*>) ^ ((f /^ k) | ((j -' k) -' 1))) ^ (<*(f /. k)*> ^ (f /^ j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
l is ext-real V24() V25() V26() V30() V31() V32() V33() set
j + l is ext-real V31() V32() V33() set
F is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
F - j is ext-real V31() V32() V33() set
j - j is ext-real V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
F -' j is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /^ F is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. j is Element of D
<*(f /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. j)] is set
{[1,(f /. j)]} is Relation-like Function-like non empty set
(F -' j) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ j) | ((F -' j) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((F -' j) -' 1) is V34() V41((F -' j) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (F -' j) -' 1 ) } is set
(f /^ j) | (Seg ((F -' j) -' 1)) is Relation-like NAT -defined Seg ((F -' j) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
f /. F is Element of D
<*(f /. F)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(f /. F)] is set
{[1,(f /. F)]} is Relation-like Function-like non empty set
j -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (j -' 1) is V34() V41(j -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= j -' 1 ) } is set
f | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,f,j,F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ <*(f /. F)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((f /^ j) | ((F -' j) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((f /^ j) | ((F -' j) -' 1))) ^ <*(f /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((f /^ j) | ((F -' j) -' 1))) ^ <*(f /. j)*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. j)*> ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((f /^ j) | ((F -' j) -' 1))) ^ (<*(f /. j)*> ^ (f /^ F)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ <*(f /. F)*>) ^ (((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
1 - 1 is ext-real V31() V32() V33() set
j - 1 is ext-real V31() V32() V33() set
k + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k + j) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k + j) - 1 is ext-real V31() V32() V33() set
k + (j - 1) is ext-real V31() V32() V33() set
k + (j -' 1) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
k -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 + (k -' 1) is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,i] is set
{[1,i]} is Relation-like Function-like non empty set
len (D,f,j,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom (D,f,j,i) is Element of K19(NAT)
(f | (j -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
len ((f | (j -' 1)) ^ <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f | (j -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (j -' 1))) + (len <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (j -' 1))) + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(j -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,j,i) /^ F is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(len ((f | (j -' 1)) ^ <*i*>)) + k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
((f | (j -' 1)) ^ <*i*>) ^ (f /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) /^ ((len ((f | (j -' 1)) ^ <*i*>)) + k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ j) /^ k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
k - 1 is ext-real V31() V32() V33() set
j + k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(j + k) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(j + k) - 1 is ext-real V31() V32() V33() set
j + (k - 1) is ext-real V31() V32() V33() set
j + (k -' 1) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,j,i) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((D,f,j,i) /^ j) | ((F -' j) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((D,f,j,i) /^ j) | (Seg ((F -' j) -' 1)) is Relation-like NAT -defined Seg ((F -' j) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
j + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
F -' (j + 1) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
((D,f,j,i) /^ j) | (F -' (j + 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (F -' (j + 1)) is V34() V41(F -' (j + 1)) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= F -' (j + 1) ) } is set
((D,f,j,i) /^ j) | (Seg (F -' (j + 1))) is Relation-like NAT -defined Seg (F -' (j + 1)) -defined NAT -defined D -valued Function-like FinSubsequence-like set
F -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(F -' 1) -' j is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
((D,f,j,i) /^ j) | ((F -' 1) -' j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((F -' 1) -' j) is V34() V41((F -' 1) -' j) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (F -' 1) -' j ) } is set
((D,f,j,i) /^ j) | (Seg ((F -' 1) -' j)) is Relation-like NAT -defined Seg ((F -' 1) -' j) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,f,j,i) | (F -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (F -' 1) is V34() V41(F -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= F -' 1 ) } is set
(D,f,j,i) | (Seg (F -' 1)) is Relation-like NAT -defined Seg (F -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((D,f,j,i) | (F -' 1)) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (j + (k -' 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (j + (k -' 1)) is V34() V41(j + (k -' 1)) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= j + (k -' 1) ) } is set
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (Seg (j + (k -' 1))) is Relation-like NAT -defined Seg (j + (k -' 1)) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (j + (k -' 1))) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ j) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (k -' 1) is V34() V41(k -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= k -' 1 ) } is set
(f /^ j) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (j -' 1)) ^ <*i*>) ^ ((f /^ j) | (k -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ ((f /^ j) | (k -' 1))) /^ (len ((f | (j -' 1)) ^ <*i*>)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*i*>) ^ (f /^ j)) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*i*> ^ (f /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ (<*i*> ^ (f /^ j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (len (f | (j -' 1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len (f | (j -' 1))) is V34() V41( len (f | (j -' 1))) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= len (f | (j -' 1)) ) } is set
((f | (j -' 1)) ^ (<*i*> ^ (f /^ j))) | (Seg (len (f | (j -' 1)))) is Relation-like NAT -defined Seg (len (f | (j -' 1))) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,f,j,i) . j is set
(D,f,j,i) /. j is Element of D
f . F is set
(D,f,j,i) . F is set
(D,f,j,i) /. F is Element of D
(D,(D,f,j,i),F,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,j,i),j,F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*((D,f,j,i) /. F)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,((D,f,j,i) /. F)] is set
{[1,((D,f,j,i) /. F)]} is Relation-like Function-like non empty set
((D,f,j,i) | (j -' 1)) ^ <*((D,f,j,i) /. F)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,j,i) | (j -' 1)) ^ <*((D,f,j,i) /. F)*>) ^ (((D,f,j,i) /^ j) | ((F -' j) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*((D,f,j,i) /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,((D,f,j,i) /. j)] is set
{[1,((D,f,j,i) /. j)]} is Relation-like Function-like non empty set
((((D,f,j,i) | (j -' 1)) ^ <*((D,f,j,i) /. F)*>) ^ (((D,f,j,i) /^ j) | ((F -' j) -' 1))) ^ <*((D,f,j,i) /. j)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((D,f,j,i) | (j -' 1)) ^ <*((D,f,j,i) /. F)*>) ^ (((D,f,j,i) /^ j) | ((F -' j) -' 1))) ^ <*((D,f,j,i) /. j)*>) ^ ((D,f,j,i) /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((f /^ j) | ((F -' j) -' 1))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((f /^ j) | ((F -' j) -' 1))) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(len f) -' j is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f /^ j) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
F -' (1 + j) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len ((f /^ j) | ((F -' j) -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len ((f | (j -' 1)) ^ <*(f /. F)*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*(f /. F)*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (j -' 1))) + (len <*(f /. F)*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,j,F) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*(f /. j)*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len ((f /^ j) | ((F -' j) -' 1))) + (len <*(f /. j)*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len ((f /^ j) | ((F -' j) -' 1))) + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
((F -' j) -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,F,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,F,j),F,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,j,F),F,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,F) | (F -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,F) | (Seg (F -' 1)) is Relation-like NAT -defined Seg (F -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((D,f,j,F) | (F -' 1)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) /^ (j + k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,j,F) | (F -' 1)) ^ <*i*>) ^ ((((f | (j -' 1)) ^ <*(f /. F)*>) ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) /^ (j + k)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) /^ (len (((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,j,F) | (F -' 1)) ^ <*i*>) ^ (((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) /^ (len (((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,F) | (k + (j -' 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (k + (j -' 1)) is V34() V41(k + (j -' 1)) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= k + (j -' 1) ) } is set
(D,f,j,F) | (Seg (k + (j -' 1))) is Relation-like NAT -defined Seg (k + (j -' 1)) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((D,f,j,F) | (k + (j -' 1))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,j,F) | (k + (j -' 1))) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(j -' 1) + k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | ((j -' 1) + k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((j -' 1) + k) is V34() V41((j -' 1) + k) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (j -' 1) + k ) } is set
((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | (Seg ((j -' 1) + k)) is Relation-like NAT -defined Seg ((j -' 1) + k) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | ((j -' 1) + k)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | ((j -' 1) + k)) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(len (f | (j -' 1))) + k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | ((len (f | (j -' 1))) + k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len (f | (j -' 1))) + k) is V34() V41((len (f | (j -' 1))) + k) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (len (f | (j -' 1))) + k ) } is set
((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | (Seg ((len (f | (j -' 1))) + k)) is Relation-like NAT -defined Seg ((len (f | (j -' 1))) + k) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | ((len (f | (j -' 1))) + k)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)))) | ((len (f | (j -' 1))) + k)) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | k is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg k is V34() V41(k) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
(<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | (Seg k) is Relation-like NAT -defined Seg k -defined NAT -defined D -valued Function-like FinSubsequence-like set
(f | (j -' 1)) ^ ((<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ ((<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | k)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ ((<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | k)) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(len <*(f /. F)*>) + (k -' 1) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | ((len <*(f /. F)*>) + (k -' 1)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((len <*(f /. F)*>) + (k -' 1)) is V34() V41((len <*(f /. F)*>) + (k -' 1)) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (len <*(f /. F)*>) + (k -' 1) ) } is set
(<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | (Seg ((len <*(f /. F)*>) + (k -' 1))) is Relation-like NAT -defined Seg ((len <*(f /. F)*>) + (k -' 1)) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(f | (j -' 1)) ^ ((<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | ((len <*(f /. F)*>) + (k -' 1))) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ ((<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | ((len <*(f /. F)*>) + (k -' 1)))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ ((<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F))) | ((len <*(f /. F)*>) + (k -' 1)))) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*(f /. F)*> ^ (((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) | (k -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ (<*(f /. F)*> ^ (((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) | (k -' 1))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*(f /. F)*> ^ (((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) | (k -' 1)))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ (<*(f /. F)*> ^ (((((f /^ j) | ((F -' j) -' 1)) ^ <*(f /. j)*>) ^ (f /^ F)) | (k -' 1)))) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F))) | (k -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F))) | (Seg (k -' 1)) is Relation-like NAT -defined Seg (k -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F))) | (k -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F))) | (k -' 1))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F))) | (k -' 1)))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((((f /^ j) | ((F -' j) -' 1)) ^ (<*(f /. j)*> ^ (f /^ F))) | (k -' 1)))) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(f /. F)*> ^ ((f /^ j) | ((F -' j) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (j -' 1)) ^ (<*(f /. F)*> ^ ((f /^ j) | ((F -' j) -' 1))) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((f /^ j) | ((F -' j) -' 1)))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ (<*(f /. F)*> ^ ((f /^ j) | ((F -' j) -' 1)))) ^ <*i*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
l is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,(D,f,j,i),k,l) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,l) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,l),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,j,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,j,i) /. l is Element of D
(D,(D,f,j,i),k,((D,f,j,i) /. l)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) /. k is Element of D
(D,(D,(D,f,j,i),k,((D,f,j,i) /. l)),l,((D,f,j,i) /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. l is Element of D
(D,(D,f,j,i),k,(f /. l)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,j,i),k,(f /. l)),l,((D,f,j,i) /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. k is Element of D
(D,(D,(D,f,j,i),k,(f /. l)),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,(f /. l)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. l)),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,k,(f /. l)),j,i),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. l)),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,k,(f /. l)),l,(f /. k)),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,j),j,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,k),i,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. k is Element of D
(D,f,i,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,i,(f /. k)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,i,j) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,i,j) /. k is Element of D
(D,(D,f,i,j),j,((D,f,i,j) /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,j) /. j is Element of D
(D,(D,(D,f,i,j),j,((D,f,i,j) /. k)),k,((D,f,i,j) /. j)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. i is Element of D
(D,(D,(D,f,i,j),j,((D,f,i,j) /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,j),j,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,i,j),j,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,j,i),j,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,j,i),j,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,i,(f /. k)),j,i),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,(f /. k)),k,(f /. i)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,i,(f /. k)),k,(f /. i)),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,k),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,f,i,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
l is ext-real V24() V25() V26() V30() V31() V32() V33() set
(D,(D,f,i,j),k,l) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,k,l) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,l),i,j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. l is Element of D
(D,f,k,(f /. l)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,f,k,(f /. l)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,i,j) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D,f,i,j) /. l is Element of D
(D,(D,f,i,j),k,((D,f,i,j) /. l)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,i,j) /. k is Element of D
(D,(D,(D,f,i,j),k,((D,f,i,j) /. l)),l,((D,f,i,j) /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f /. k is Element of D
(D,(D,(D,f,i,j),k,((D,f,i,j) /. l)),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,i,j),k,(f /. l)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,i,j),k,(f /. l)),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,f,j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,j,i),k,(f /. l)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,j,i),k,(f /. l)),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. l)),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,k,(f /. l)),j,i),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,(f /. l)),l,(f /. k)) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,(D,f,k,(f /. l)),l,(f /. k)),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,(D,f,k,l),j,i) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D