let h be complex-valued FinSequence; :: thesis: (h,1) +...+ (h,(len h)) = Sum h
set L = len h;

per cases ( len h >= 1 or len h < 1 ) ;

suppose A1: len h >= 1 ; :: thesis: (h,1) +...+ (h,(len h)) = Sum h

then consider w being complex-valued FinSequence such that
A2: ( (h,1) +...+ (h,(len h)) = Sum w & len w = ((len h) -' 1) + 1 ) and
A3: w . (0 + 1) = h . (0 + 1) & ... & w . (((len h) -' 1) + 1) = h . (((len h) -' 1) + 1) by Th9;
A4: ((len h) -' 1) + 1 = ((len h) - 1) + 1 by A1, NAT_D:34;

now :: thesis: for i being Nat st 1 <= i & i <= len h holds
h . i = w . i

let i be Nat; :: thesis: ( 1 <= i & i <= len h implies h . i = w . i )
assume A5: ( 1 <= i & i <= len h ) ; :: thesis: h . i = w . i
reconsider i1 = i - 1 as Nat by A5;
w . (i1 + 1) = h . (i1 + 1) by A4, A5, XREAL_1:6, A3;
hence h . i = w . i ; :: thesis: verum

end;

then h = w by A4, A2;
hence (h,1) +...+ (h,(len h)) = Sum h by A2; :: thesis: verum

end;

suppose len h < 1 ; :: thesis: (h,1) +...+ (h,(len h)) = Sum h

then h = <*> REAL by FINSEQ_1:20;
hence (h,1) +...+ (h,(len h)) = Sum h by RVSUM_1:72, Def1; :: thesis: verum

end;

end;