let k, n be Nat; :: thesis: for h being complex-valued FinSequence st k > len h holds
(h,k) +...+ (h,n) = 0
let h be complex-valued FinSequence; :: thesis: ( k > len h implies (h,k) +...+ (h,n) = 0 )
assume A1: k > len h ; :: thesis: (h,k) +...+ (h,n) = 0

per cases ( k > n or k <= n ) ;

suppose k > n ; :: thesis: (h,k) +...+ (h,n) = 0

hence (h,k) +...+ (h,n) = 0 by Def1; :: thesis: verum

end;

suppose k <= n ; :: thesis: (h,k) +...+ (h,n) = 0

then consider w being complex-valued FinSequence such that
A2: ( (h,k) +...+ (h,n) = Sum w & len w = (n -' k) + 1 ) and
A3: w . (0 + 1) = h . (0 + k) & ... & w . ((n -' k) + 1) = h . ((n -' k) + k) by Th9;
set nk = (n -' k) + 1;
set nk0 = ((n -' k) + 1) |-> 0;

now :: thesis: for i being Nat st 1 <= i & i <= (n -' k) + 1 holds
w . i = (((n -' k) + 1) |-> 0) . i

let i be Nat; :: thesis: ( 1 <= i & i <= (n -' k) + 1 implies w . i = (((n -' k) + 1) |-> 0) . i )
assume A4: ( 1 <= i & i <= (n -' k) + 1 ) ; :: thesis: w . i = (((n -' k) + 1) |-> 0) . i
reconsider i1 = i - 1 as Nat by A4;
i1 + 1 = i ;
then i1 <= n -' k by A4, XREAL_1:6;
then A5: w . (i1 + 1) = h . (i1 + k) by A3;
i1 + k > 0 + (len h) by A1, XREAL_1:8;
then not i1 + k in dom h by FINSEQ_3:25;
hence w . i = (((n -' k) + 1) |-> 0) . i by FUNCT_1:def 2, A5; :: thesis: verum

end;

then w = ((n -' k) + 1) |-> 0 by CARD_1:def 7, A2;
then Sum w = ((n -' k) + 1) * 0 by RVSUM_1:80;
hence (h,k) +...+ (h,n) = 0 by A2; :: thesis: verum

end;

end;