for seq being ExtREAL_sequence holds Ser seq = Partial_Sums seq