theorem :: COMSEQ_2:41

for s, s9 being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *')