let f, g be eventually-positive Real_Sequence; :: thesis:
assume A1: ( f /" g is convergent & lim (f /" g) > 0 ) ; :: thesis:
set l = lim (f /" g);
set delta = lim (f /" g);
set c = 2 * (lim (f /" g));
A2: 2 * (lim (f /" g)) > 2 * 0 by A1, XREAL_1:70;
consider N being Element of NAT such that
A3: for n being Element of NAT st N <= n holds
abs (((f /" g) . n) - (lim (f /" g))) < lim (f /" g) by A1, SEQ_2:def 7;
A4: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
consider N1 being Element of NAT such that
A5: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A6: for n being Element of NAT st n >= N2 holds
g . n > 0 by Def6;
set b = max N,N1;
set a = max (max N,N1),N2;

let n be Element of NAT ; :: thesis:
assume A7: n >= max (max N,N1),N2 ; :: thesis:
A8: ( max (max N,N1),N2 >= max N,N1 & max (max N,N1),N2 >= N2 ) by XXREAL_0:25;
A9: ( max N,N1 >= N & max N,N1 >= N1 ) by XXREAL_0:25;
n >= max N,N1 by A7, A8, XXREAL_0:2;
then A10: ( n >= N & n >= N1 & n >= N2 ) by A7, A8, A9, XXREAL_0:2;
then abs (((f /" g) . n) - (lim (f /" g))) < lim (f /" g) by A3;
then ((f /" g) . n) - (lim (f /" g)) <= lim (f /" g) by ABSVALUE:12;
then (f /" g) . n <= (1 * (lim (f /" g))) + (1 * (lim (f /" g))) by XREAL_1:22;
then (f . n) * ((g " ) . n) <= 2 * (lim (f /" g)) by SEQ_1:12;
then A11: (f . n) * ((g . n) " ) <= 2 * (lim (f /" g)) by VALUED_1:10;
A12: g . n > 0 by A6, A10;
then ((f . n) * ((g . n) " )) * (g . n) <= (2 * (lim (f /" g))) * (g . n) by A11, XREAL_1:66;
then (f . n) * (((g . n) " ) * (g . n)) <= (2 * (lim (f /" g))) * (g . n) ;
then (f . n) * 1 <= (2 * (lim (f /" g))) * (g . n) by A12, XCMPLX_0:def 7;
hence f . n <= (2 * (lim (f /" g))) * (g . n) ; :: thesis:
thus f . n >= 0 by A5, A10; :: thesis:

end;

hence f in Big_Oh g by A2, A4; :: thesis: