let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is convergent holds
- seq is convergent
let seq be sequence of X; :: thesis: ( seq is convergent implies - seq is convergent )
assume seq is convergent ; :: thesis: - seq is convergent
then (- 1r) * seq is convergent by Th5;
hence - seq is convergent by CSSPACE:70; :: thesis: verum