let s be convergent Complex_Sequence; :: thesis: lim ((- s) *') = - ((lim s) *')
thus lim ((- s) *') = (lim (- s)) *' by Th12
.= (- (lim s)) *' by Th22
.= - ((lim s) *') by COMPLEX1:33 ; :: thesis: verum