let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)
let seq be sequence of X; :: thesis: Partial_Sums (- seq) = - (Partial_Sums seq)
Partial_Sums ((- 1) * seq) = (- 1) * (Partial_Sums seq) by Th3;
then Partial_Sums (- seq) = (- 1) * (Partial_Sums seq) by BHSP_1:55;
hence Partial_Sums (- seq) = - (Partial_Sums seq) by BHSP_1:55; :: thesis: verum