let X be RealUnitarySpace; :: 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 (- 1) * seq is Cauchy by Th5;
hence - seq is Cauchy by BHSP_1:77; :: thesis: verum