for f being eventually-nonnegative Real_Sequence
for c being positive Real holds Big_Oh f = Big_Oh (c (#) f)