theorem :: ASYMPT_0:41

for f, g being eventually-nonnegative Real_Sequence holds (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g)