theorem :: SEQ_2:32

for s, s9 being convergent Complex_Sequence holds lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).|