for s1, s2 being Real_Sequence holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)