let k, n be Nat; :: thesis: 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) )
let f be complex-valued Function; :: thesis: ( k <= n implies 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) ) )
assume A1: k <= n ; :: thesis: 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) )
deffunc H₁( Nat) -> set = f . ((k + $1) - 1);
set nk = (n -' k) + 1;
consider p being FinSequence such that
A2: ( len p = (n -' k) + 1 & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_1:sch 2();
rng p c= COMPLEX

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in COMPLEX )
assume y in rng p ; :: thesis: y in COMPLEX
then consider x being object such that
A4: ( x in dom p & p . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A4;
p . x = f . ((k + x) - 1) by A4, A2;
hence y in COMPLEX by A4, XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider p = p as complex-valued FinSequence by VALUED_0:def 1;
A5: p . (1 + 0) = f . (k + 0) & ... & p . (1 + (n -' k)) = f . (k + (n -' k))

proof

let i be Nat; :: thesis: ( not 0 <= i or not i <= n -' k or p . (1 + i) = f . (k + i) )
assume ( 0 <= i & i <= n -' k ) ; :: thesis: p . (1 + i) = f . (k + i)
then ( 1 <= i + 1 & i + 1 <= (n -' k) + 1 ) by NAT_1:11, XREAL_1:6;
then p . (i + 1) = f . ((k + (i + 1)) - 1) by A2, FINSEQ_3:25;
hence p . (1 + i) = f . (k + i) ; :: thesis: verum

end;

then (f,k) +...+ (f,n) = Sum (p | ((n -' k) + 1)) by A1, Def1;
then Sum p = (f,k) +...+ (f,n) by FINSEQ_1:58, A2;
hence 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) ) by A2, A5; :: thesis: verum