let X be ComplexUnitarySpace; :: 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 ((- 1r ) * seq) = (- 1r ) * (lim seq) by Th15;
then lim (- seq) = (- 1r ) * (lim seq) by CSSPACE:77;
hence lim (- seq) = - (lim seq) by CLVECT_1:4; :: thesis: verum