for c being non negative Real
for x, f being eventually-nonnegative Real_Sequence st ex e being Real ex N being Element of NAT st
( e > 0 & ( for n being Element of NAT st n >= N holds
f . n >= e ) ) & x in Big_Oh (c + f) holds
x in Big_Oh f