theorem :: RVSUM_4:4

for s being Real_Sequence
for n being Nat holds (Partial_Sums s) . n = Sum (s | (Segm (n + 1))) by AFINSQ_2:56;