theorem :: BHSP_4:4

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