for s, s9 being convergent Complex_Sequence holds lim |.(s + s9).| = |.((lim s) + (lim s9)).|