theorem :: SEQ_2:34

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).|