theorem Th2: :: CLVECT_3:2

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