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