let f, g be eventually-positive Real_Sequence; :: thesis:
assume that
A1: f /" g is convergent and
A2: lim (f /" g) > 0 ; :: thesis:
set l = lim (f /" g);
set delta = lim (f /" g);
set c = 2 * (lim (f /" g));
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, A2, SEQ_2:def 7;
consider N2 being Element of NAT such that
A4: for n being Element of NAT st n >= N2 holds
g . n > 0 by Def6;
consider N1 being Element of NAT such that
A5: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
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:
max ((max (N,N1)),N2) >= N2 by XXREAL_0:25;
then n >= N2 by A7, XXREAL_0:2;
then A8: g . n > 0 by A4;
max ((max (N,N1)),N2) >= max (N,N1) by XXREAL_0:25;
then A9: n >= max (N,N1) by A7, XXREAL_0:2;
max (N,N1) >= N by XXREAL_0:25;
then n >= N by 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: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:
max (N,N1) >= N1 by XXREAL_0:25;
then n >= N1 by A9, XXREAL_0:2;
hence f . n >= 0 by A5; :: thesis:

end;