theorem Th1: :: BHSP_4:1

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