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