let r be real number ; :: thesis: for s being convergent Complex_Sequence holds lim |.(r (#) s).| = |.r.| * |.(lim s).|
let s be convergent Complex_Sequence; :: thesis: lim |.(r (#) s).| = |.r.| * |.(lim s).|
thus lim |.(r (#) s).| = |.(lim (r (#) s)).| by Th27
.= |.(r * (lim s)).| by COMSEQ_2:18
.= |.r.| * |.(lim s).| by COMPLEX1:65 ; :: thesis: verum