for seq being ExtREAL_sequence
for n being Nat holds (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n)