let s be Complex_Sequence; :: thesis: ( s is convergent implies lim (- s) = - (lim s) )
assume s is convergent ; :: thesis: lim (- s) = - (lim s)
then lim (- s) = (- 1) * (lim s) by Th18
.= - (1r * (lim s)) by COMPLEX1:def 7 ;
hence lim (- s) = - (lim s) by COMPLEX1:def 7; :: thesis: verum