theorem :: SEQ_2:31

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