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:26 ; :: thesis: verum