let k, n be Nat; :: thesis: for f being complex-valued Function st k <= n holds
(f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))
let f be complex-valued Function; :: thesis: ( k <= n implies (f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n)) )
set k1 = k + 1;
assume A1: k <= n ; :: thesis: (f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))

per cases ( k = n or k < n ) by A1, XXREAL_0:1;

suppose A2: k = n ; :: thesis: (f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))

then A3: k + 1 > n by NAT_1:13;
thus (f,k) +...+ (f,n) = (f . k) + 0 by A2, Th11
.= (f . k) + ((f,(k + 1)) +...+ (f,n)) by A3, Def1 ; :: thesis: verum

end;

suppose A4: k < n ; :: thesis: (f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))

then k + 1 <= n by NAT_1:13;
then consider h being complex-valued FinSequence such that
A5: ( (f,(k + 1)) +...+ (f,n) = Sum h & len h = (n -' (k + 1)) + 1 ) and
A6: h . (0 + 1) = f . (0 + (k + 1)) & ... & h . ((n -' (k + 1)) + 1) = f . ((n -' (k + 1)) + (k + 1)) by Th9;
reconsider fk = f . k as Complex ;
set h1 = <*fk*> ^ h;
A7: (n -' (k + 1)) + 1 = n -' k by A4, NAT_D:59;
A8: len <*fk*> = 1 by FINSEQ_1:39;
then len (<*fk*> ^ h) = (n -' k) + 1 by FINSEQ_1:22, A7, A5;
then A9: (<*fk*> ^ h) | ((n -' k) + 1) = <*fk*> ^ h by FINSEQ_1:58;
(<*fk*> ^ h) . (0 + 1) = f . (0 + k) & ... & (<*fk*> ^ h) . ((n -' k) + 1) = f . ((n -' k) + k)

proof

let i be Nat; :: thesis: ( not 0 <= i or not i <= n -' k or (<*fk*> ^ h) . (i + 1) = f . (i + k) )
set i1 = i + 1;
assume A10: ( 0 <= i & i <= n -' k ) ; :: thesis: (<*fk*> ^ h) . (i + 1) = f . (i + k)

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: (<*fk*> ^ h) . (i + 1) = f . (i + k)

hence (<*fk*> ^ h) . (i + 1) = f . (i + k) by FINSEQ_1:41; :: thesis: verum

end;

suppose A11: i > 0 ; :: thesis: (<*fk*> ^ h) . (i + 1) = f . (i + k)

then reconsider ii = i - 1 as Nat ;
ii + 1 <= (n -' (k + 1)) + 1 by A4, NAT_D:59, A10;
then ii <= n -' (k + 1) by XREAL_1:6;
then A12: h . (ii + 1) = f . (ii + (k + 1)) by A6;
i >= 1 by NAT_1:14, A11;
then i in dom h by A5, A7, A10, FINSEQ_3:25;
hence (<*fk*> ^ h) . (i + 1) = f . (i + k) by A8, FINSEQ_1:def 7, A12; :: thesis: verum

end;

end;

end;

hence (f,k) +...+ (f,n) = Sum (<*fk*> ^ h) by Def1, A4, A9
.= (f . k) + ((f,(k + 1)) +...+ (f,n)) by RVSUM_2:33, A5 ;
:: thesis: verum

end;

end;