theorem Th5: :: MESFUN9C:5

for seq being Real_Sequence holds Partial_Sums (R_EAL seq) = R_EAL (Partial_Sums seq)