theorem :: SEQ_2:24

for seq, seq9 being Real_Sequence st seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero holds
lim (seq9 /" seq) = (lim seq9) / (lim seq)