let X be ComplexUnitarySpace; :: 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 ((- 1r) * seq) = (- 1r) * (Partial_Sums seq) by Th3;
then Partial_Sums (- seq) = (- 1r) * (Partial_Sums seq) by CSSPACE:70;
hence Partial_Sums (- seq) = - (Partial_Sums seq) by CSSPACE:70; :: thesis: verum