let s be convergent Complex_Sequence; :: thesis: lim (- s) = - (lim s)
lim (- s) = (- 1) * (lim s) by Th18
.= - (1r * (lim s)) by COMPLEX1:def 4 ;
hence lim (- s) = - (lim s) by COMPLEX1:def 4; :: thesis: verum