theorem :: COMSEQ_2:45
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim ((s (#) s1) *') = 0c