for f being Real_Sequence
for n being Nat st f . 0 = 0 holds
Sum (f |_ (Seg n)) = (Partial_Sums f) . n