theorem Th20: :: COMSEQ_2:30

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