theorem Th5: :: ASYMPT_0:5

for f being Real_Sequence

for g being eventually-nonzero Real_Sequence st f /" g is divergent_to+infty holds

( g /" f is convergent & lim (g /" f) = 0 )

for g being eventually-nonzero Real_Sequence st f /" g is divergent_to+infty holds

( g /" f is convergent & lim (g /" f) = 0 )