let s be Complex_Sequence; :: thesis: ( s is convergent implies lim |.(- s).| = |.(lim s).| )
assume A1: s is convergent ; :: thesis: lim |.(- s).| = |.(lim s).|
then - s is convergent ;
hence lim |.(- s).| = |.(lim (- s)).| by Th11
.= |.(- (lim s)).| by A1, Th22
.= |.(lim s).| by COMPLEX1:138 ;
:: thesis: verum