let X be RealUnitarySpace; :: 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 (- 1) * seq is convergent by Th5;

hence - seq is convergent by BHSP_1:55; :: thesis: verum

- 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 (- 1) * seq is convergent by Th5;

hence - seq is convergent by BHSP_1:55; :: thesis: verum