theorem
:: ASYMPT_0:14
for
c
being non
negative
Real
for
x
,
f
being
eventually-nonnegative
Real_Sequence
st
x
in
Big_Oh
f
holds
x
in
Big_Oh
(
c
+
f
)