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:119 ;
:: thesis: verum