theorem :: ASYMPT_0:32

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