theorem
Th36
:
:: ASYMPT_0:36
for
f
being
eventually-nonnegative
Real_Sequence
for
X
being
set
holds
Big_Theta
(
f
,
X
)
=
(
Big_Oh
(
f
,
X
)
)
/\
(
Big_Omega
(
f
,
X
)
)