theorem Th1: :: CLVECT_3:1

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)