theorem
:: ASYMPT_0:30
for
f
,
g
,
h
being
eventually-nonnegative
Real_Sequence
st
f
in
Big_Theta
g
&
g
in
Big_Theta
h
holds
f
in
Big_Theta
h