let n be Nat; :: thesis: for f being FinSequence of REAL n st len f > 0 holds
(accum f) . (len f) = Sum f
let f be FinSequence of REAL n; :: thesis: ( len f > 0 implies (accum f) . (len f) = Sum f )
assume A1: len f > 0 ; :: thesis: (accum f) . (len f) = Sum f
A2: ( len f = len (accum f) & f . 1 = (accum f) . 1 & ( for i being Nat st 1 <= i & i < len f holds
(accum f) . (i + 1) = ((accum f) /. i) + (f /. (i + 1)) ) ) by Def12;
A3: ( len f = len (accum f) & f . 1 = (accum f) . 1 & ( for i being Nat st 1 <= i & i < len f holds
(accum f) . (i + 1) = ((accum f) /. i) + (f /. (i + 1)) ) & (accum f) . (len f) = (accum f) . (len f) ) by Def12;
0 + 1 <= len f by A1, NAT_1:13;
then (accum f) /. (len f) = (accum f) . (len f) by A2, FINSEQ_4:24;
hence (accum f) . (len f) = Sum f by A1, A3, Def11; :: thesis: verum