theorem Th6: :: ASYMPT_0:6

for x being set

for f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds

x is eventually-nonnegative Real_Sequence

for f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds

x is eventually-nonnegative Real_Sequence