theorem Th2: :: BHSP_4:2

for X being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)