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:30
.= |.(lim s).| * |.(lim s9).| by COMPLEX1:65 ; :: thesis: verum