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