let s be convergent Complex_Sequence; :: thesis: lim |.(- s).| = |.(lim s).|
thus lim |.(- s).| = |.(lim (- s)).| by Th27
.= |.(- (lim s)).| by COMSEQ_2:22
.= |.(lim s).| by COMPLEX1:52 ; :: thesis: verum