let f be eventually-nonnegative Real_Sequence; :: thesis: f in Big_Oh f
A1: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
consider N being Element of NAT such that
A2: for n being Element of NAT st n >= N holds
f . n >= 0 by Def4;
for n being Element of NAT st n >= N holds
( f . n <= 1 * (f . n) & f . n >= 0 ) by A2;
hence f in Big_Oh f by A1; :: thesis: verum