for s being Complex_Sequence st s is convergent holds
lim |.s.| = |.(lim s).|