theorem
Th23
:
:: ASYMPT_0:23
for
f
,
g
being
eventually-positive
Real_Sequence
st
f
/"
g
is
convergent
&
lim
(
f
/"
g
)
=
0
holds
(
g
in
Big_Omega
f
& not
f
in
Big_Omega
g
)