theorem :: CLVECT_3:4

for X being ComplexUnitarySpace
for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)