theorem Th27: :: COMSEQ_2:39

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)