let seq be Real_Sequence; :: 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 Th22;
hence lim (- seq) = - (lim seq) ; :: thesis: verum