theorem :: SEQ_2:29

for r being Real
for s being convergent Complex_Sequence holds lim |.(r (#) s).| = |.r.| * |.(lim s).|