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

per cases ( k = n + 1 or k <= n ) by A1, NAT_1:8;

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

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

end;

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

then consider h being complex-valued FinSequence such that
A4: ( (f,k) +...+ (f,n) = Sum h & len h = (n -' k) + 1 ) and
A5: h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) by Th9;
A6: (n + 1) -' k = (n -' k) + 1 by A3, NAT_D:38;
set fn = f . (n + 1);
reconsider fn = f . (n + 1) as Complex ;
set h1 = h ^ <*fn*>;
A7: len (h ^ <*fn*>) = ((n + 1) -' k) + 1 by A6, A4, FINSEQ_2:16;
(h ^ <*fn*>) . (0 + 1) = f . (0 + k) & ... & (h ^ <*fn*>) . (((n + 1) -' k) + 1) = f . (((n + 1) -' k) + k)

proof

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

per cases ( i <= n -' k or i = (n -' k) + 1 ) by A8, A6, NAT_1:8;

suppose A9: i <= n -' k ; :: thesis: (h ^ <*fn*>) . (i + 1) = f . (i + k)

then ( 1 <= i + 1 & i + 1 <= len h ) by NAT_1:11, A4, XREAL_1:6;
then i + 1 in dom h by FINSEQ_3:25;
then (h ^ <*fn*>) . (i + 1) = h . (i + 1) by FINSEQ_1:def 7;
hence (h ^ <*fn*>) . (i + 1) = f . (i + k) by A5, A9; :: thesis: verum

end;

suppose A10: i = (n -' k) + 1 ; :: thesis: (h ^ <*fn*>) . (i + 1) = f . (i + k)

((n + 1) -' k) + k = ((n + 1) - k) + k by NAT_D:37, A3;
hence (h ^ <*fn*>) . (i + 1) = f . (i + k) by A10, A4, FINSEQ_1:42, A6; :: thesis: verum

end;

end;

end;

then (f,k) +...+ (f,(n + 1)) = Sum ((h ^ <*fn*>) | (((n + 1) -' k) + 1)) by A1, Def1
.= Sum (h ^ <*fn*>) by A7, FINSEQ_1:58 ;
hence (f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1)) by A4, RVSUM_2:31; :: thesis: verum

end;

end;