theorem Th12: :: ASYMPT_0:12

for f, g, h being eventually-nonnegative Real_Sequence st f in Big_Oh g & g in Big_Oh h holds
f in Big_Oh h