let f be eventually-nonnegative Real_Sequence; :: thesis: f in Big_Oh f
consider N being Nat such that
A1: for n being Nat st n >= N holds
f . n >= 0 by Def2;
reconsider N = N as Element of NAT by ORDINAL1:def 12;
( f is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= N holds
( f . n <= 1 * (f . n) & f . n >= 0 ) ) ) by A1, FUNCT_2:8;
hence f in Big_Oh f ; :: thesis: verum