theorem Th21: :: LIOUVIL1:21

for f being Real_Sequence
for n being Nat st f . 0 = 0 holds
Sum (FinSeq (f,n)) = (Partial_Sums f) . n