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 )
A1: len f = len (accum f) by Def11;
assume A2: len f > 0 ; :: thesis: (accum f) . (len f) = Sum f
then 0 + 1 <= len f by NAT_1:13;
then A3: (accum f) /. (len f) = (accum f) . (len f) by A1, FINSEQ_4:24;
A4: for i being Nat st 1 <= i & i < len f holds
(accum f) . (i + 1) = ((accum f) /. i) + (f /. (i + 1)) by Def11;
A5: f . 1 = (accum f) . 1 by Def11;
len f = len (accum f) by Def11;
hence (accum f) . (len f) = Sum f by A2, A5, A4, A3, Def10; :: thesis: verum