let s be Complex_Sequence; :: thesis: ( s is convergent implies lim ((- s) *') = - ((lim s) *') )
assume A1: s is convergent ; :: thesis: lim ((- s) *') = - ((lim s) *')
hence lim ((- s) *') = (lim (- s)) *' by Th12
.= (- (lim s)) *' by A1, Th22
.= - ((lim s) *') by COMPLEX1:33 ;
:: thesis: verum