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 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;

let n be Element of NAT ; :: thesis:
assume A7: n >= a ; :: thesis:
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:
b >= N1 by XXREAL_0:25;
then n >= N1 by A9, XXREAL_0:2;
hence f . n >= 0 by A5; :: thesis:

end;