let X be RealUnitarySpace; :: thesis: for seq being sequence of X st seq is convergent holds

lim (- seq) = - (lim seq)

let seq be sequence of X; :: thesis: ( seq is convergent implies lim (- seq) = - (lim seq) )

assume seq is convergent ; :: thesis: lim (- seq) = - (lim seq)

then lim ((- 1) * seq) = (- 1) * (lim seq) by Th15;

then lim (- seq) = (- 1) * (lim seq) by BHSP_1:55;

hence lim (- seq) = - (lim seq) by RLVECT_1:16; :: thesis: verum

lim (- seq) = - (lim seq)

let seq be sequence of X; :: thesis: ( seq is convergent implies lim (- seq) = - (lim seq) )

assume seq is convergent ; :: thesis: lim (- seq) = - (lim seq)

then lim ((- 1) * seq) = (- 1) * (lim seq) by Th15;

then lim (- seq) = (- 1) * (lim seq) by BHSP_1:55;

hence lim (- seq) = - (lim seq) by RLVECT_1:16; :: thesis: verum