let f be Real_Sequence; :: thesis: for g being eventually-nonzero Real_Sequence st f /" g is divergent_to+infty holds
( g /" f is convergent & lim (g /" f) = 0 )
let g be eventually-nonzero Real_Sequence; :: thesis: ( f /" g is divergent_to+infty implies ( g /" f is convergent & lim (g /" f) = 0 ) )
consider N1 being Nat such that
A1: for n being Nat st n >= N1 holds
g . n <> 0 by Def5;
assume A2: f /" g is divergent_to+infty ; :: thesis: ( g /" f is convergent & lim (g /" f) = 0 )

A3: now :: thesis: for p being Real st p > 0 holds
ex a being Nat st
for n being Nat st n >= a holds
|.(((g /" f) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex a being Nat st
for n being Nat st n >= a holds
|.(((g /" f) . b₅) - 0).| < b₃ )
assume A4: p > 0 ; :: thesis: ex a being Nat st
for n being Nat st n >= a holds
|.(((g /" f) . b₅) - 0).| < b₃
reconsider w = 1 / p as Real ;
consider N being Nat such that
A5: for n being Nat st n >= N holds
w < (f /" g) . n by A2, LIMFUNC1:def 4;
reconsider a = max (N,N1) as Nat by TARSKI:1;
take a = a; :: thesis: for n being Nat st n >= a holds
|.(((g /" f) . b₄) - 0).| < b₂
let n be Nat; :: thesis: ( n >= a implies |.(((g /" f) . b₃) - 0).| < b₁ )
assume A6: n >= a ; :: thesis: |.(((g /" f) . b₃) - 0).| < b₁
a >= N by XXREAL_0:25;
then n >= N by A6, XXREAL_0:2;
then 1 / p < (f /" g) . n by A5;
then (1 / p) * p < p * ((f /" g) . n) by A4, XREAL_1:68;
then 1 < p * ((f /" g) . n) by A4, XCMPLX_1:106;
then A7: 1 < p * ((f . n) / (g . n)) by Lm1;
then A8: 1 < p * ((f . n) * ((g . n) ")) by XCMPLX_0:def 9;

A9: now :: thesis: ( (g . n) * ((f . n) ") > (g . n) * 0 implies ((g /" f) . n) - 0 >= 0 )

assume (g . n) * ((f . n) ") > (g . n) * 0 ; :: thesis: ((g /" f) . n) - 0 >= 0
then (g . n) * ((f ") . n) > 0 by VALUED_1:10;
hence ((g /" f) . n) - 0 >= 0 by SEQ_1:8; :: thesis: verum

end;

a >= N1 by XXREAL_0:25;
then A10: g . n <> 0 by A1, A6, XXREAL_0:2;
A11: f . n <> 0 by A7;

A12: now :: thesis: ( (g . n) * ((f . n) ") < (p * (f . n)) * ((f . n) ") implies ((g /" f) . n) - 0 < p )

assume (g . n) * ((f . n) ") < (p * (f . n)) * ((f . n) ") ; :: thesis: ((g /" f) . n) - 0 < p
then (g . n) * ((f ") . n) < (p * (f . n)) * ((f . n) ") by VALUED_1:10;
then (g (#) (f ")) . n < p * ((f . n) * ((f . n) ")) by SEQ_1:8;
then (g (#) (f ")) . n < p * 1 by A11, XCMPLX_0:def 7;
hence ((g /" f) . n) - 0 < p ; :: thesis: verum

end;

per cases ( g . n > 0 or g . n < 0 ) by A10;

suppose A13: g . n > 0 ; :: thesis: |.(((g /" f) . b₃) - 0).| < b₁

then 1 * (g . n) < ((p * (f . n)) * ((g . n) ")) * (g . n) by A8, XREAL_1:68;
then g . n < (p * (f . n)) * (((g . n) ") * (g . n)) ;
then A14: g . n < (p * (f . n)) * 1 by A10, XCMPLX_0:def 7;
f . n > 0 by A4, A7, A13;
hence |.(((g /" f) . n) - 0).| < p by A12, A9, A13, A14, ABSVALUE:def 1, XREAL_1:68; :: thesis: verum

end;

suppose A15: g . n < 0 ; :: thesis: |.(((g /" f) . b₃) - 0).| < b₁

then 1 * (g . n) > ((p * (f . n)) * ((g . n) ")) * (g . n) by A8, XREAL_1:69;
then g . n > (p * (f . n)) * (((g . n) ") * (g . n)) ;
then A16: g . n > (p * (f . n)) * 1 by A10, XCMPLX_0:def 7;
f . n < 0 by A4, A7, A15;
hence |.(((g /" f) . n) - 0).| < p by A12, A9, A15, A16, ABSVALUE:def 1, XREAL_1:69; :: thesis: verum

end;

end;

end;

hence g /" f is convergent by SEQ_2:def 6; :: thesis: lim (g /" f) = 0
hence lim (g /" f) = 0 by A3, SEQ_2:def 7; :: thesis: verum