let s, s9 be convergent Complex_Sequence; :: thesis: lim |.(s + s9).| = |.((lim s) + (lim s9)).|
thus lim |.(s + s9).| = |.(lim (s + s9)).| by Th27
.= |.((lim s) + (lim s9)).| by COMSEQ_2:14 ; :: thesis: verum