theorem Th1: :: DBLSEQ_3:1

for seq being ExtREAL_sequence holds Partial_Sums (- seq) = - (Partial_Sums seq)