let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) > 0 implies f in Big_Oh g )
assume that
A1: f /" g is convergent and
A2: lim (f /" g) > 0 ; :: thesis: f in Big_Oh g
set l = lim (f /" g);
set delta = lim (f /" g);
set c = 2 * (lim (f /" g));
consider N being Nat such that
A3: for n being Nat st N <= n holds
|.(((f /" g) . n) - (lim (f /" g))).| < lim (f /" g) by A1, A2, SEQ_2:def 7;
consider N2 being Nat such that
A4: for n being Nat st n >= N2 holds
g . n > 0 by Def4;
consider N1 being Nat such that
A5: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
reconsider b = max (N,N1) as Element of NAT by ORDINAL1:def 12;
reconsider a = max (b,N2) as Element of NAT by ORDINAL1:def 12;

A6: now :: thesis: for n being Element of NAT st n >= a holds
( f . n <= (2 * (lim (f /" g))) * (g . n) & f . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= a implies ( f . n <= (2 * (lim (f /" g))) * (g . n) & f . n >= 0 ) )
assume A7: n >= a ; :: thesis: ( f . n <= (2 * (lim (f /" g))) * (g . n) & f . n >= 0 )
a >= N2 by XXREAL_0:25;
then n >= N2 by A7, XXREAL_0:2;
then A8: g . n > 0 by A4;
a >= b by XXREAL_0:25;
then A9: n >= b by A7, XXREAL_0:2;
b >= N by XXREAL_0:25;
then n >= N by A9, XXREAL_0:2;
then |.(((f /" g) . n) - (lim (f /" g))).| < lim (f /" g) by A3;
then ((f /" g) . n) - (lim (f /" g)) <= lim (f /" g) by ABSVALUE:5;
then (f /" g) . n <= (1 * (lim (f /" g))) + (1 * (lim (f /" g))) by XREAL_1:20;
then (f . n) * ((g ") . n) <= 2 * (lim (f /" g)) by SEQ_1:8;
then (f . n) * ((g . n) ") <= 2 * (lim (f /" g)) by VALUED_1:10;
then ((f . n) * ((g . n) ")) * (g . n) <= (2 * (lim (f /" g))) * (g . n) by A8, XREAL_1:64;
then (f . n) * (((g . n) ") * (g . n)) <= (2 * (lim (f /" g))) * (g . n) ;
then (f . n) * 1 <= (2 * (lim (f /" g))) * (g . n) by A8, XCMPLX_0:def 7;
hence f . n <= (2 * (lim (f /" g))) * (g . n) ; :: thesis: f . n >= 0
b >= N1 by XXREAL_0:25;
then n >= N1 by A9, XXREAL_0:2;
hence f . n >= 0 by A5; :: thesis: verum

end;

A10: f is Element of Funcs (NAT,REAL) by FUNCT_2:8;
2 * (lim (f /" g)) > 2 * 0 by A2, XREAL_1:68;
hence f in Big_Oh g by A10, A6; :: thesis: verum