theorem Th38: :: ASYMPT_0:38

for f being eventually-nonnegative Real_Sequence

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Nat st f is smooth & b >= 2 & t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Oh f

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Nat st f is smooth & b >= 2 & t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Oh f