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:77;
hence Partial_Sums (- seq) = - (Partial_Sums seq) by CSSPACE:77; :: thesis: verum