for s being Real_Sequence
for n being Nat holds (Partial_Sums s) . n = Sum (Shift ((s | (Segm (n + 1))),1))