theorem
:: ASYMPT_0:32
for
f
,
g
being
eventually-nonnegative
Real_Sequence
holds
Big_Theta
(
f
+
g
)
=
Big_Theta
(
max
(
f
,
g
)
)