for k, n being Nat
for f being complex-valued Function st k <= n holds
ex h being complex-valued FinSequence st
( (f,k) +...+ (f,n) = Sum h & len h = (n -' k) + 1 & h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) )