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 ) )
assume A1: f /" g is divergent_to+infty ; :: thesis: ( g /" f is convergent & lim (g /" f) = 0 )
consider N1 being Element of NAT such that
A2: for n being Element of NAT st n >= N1 holds
g . n <> 0 by Def7;

A3: now

let p be real number ; :: thesis: ( p > 0 implies ex a being Element of NAT st
for n being Element of NAT st n >= a holds
abs (((g /" f) . b₅) - 0 ) < b₃ )
assume A4: p > 0 ; :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a holds
abs (((g /" f) . b₅) - 0 ) < b₃
reconsider w = 1 / p as Real ;
consider N being Element of NAT such that
A5: for n being Element of NAT st n >= N holds
w < (f /" g) . n by A1, LIMFUNC1:def 4;
set a = max N,N1;
A6: ( max N,N1 >= N & max N,N1 >= N1 ) by XXREAL_0:25;
take a = max N,N1; :: thesis: for n being Element of NAT st n >= a holds
abs (((g /" f) . b₄) - 0 ) < b₂
let n be Element of NAT ; :: thesis: ( n >= a implies abs (((g /" f) . b₃) - 0 ) < b₁ )
assume A7: n >= a ; :: thesis: abs (((g /" f) . b₃) - 0 ) < b₁
then ( n >= N & n >= N1 ) by A6, XXREAL_0:2;
then A8: 1 / p < (f /" g) . n by A5;
A9: g . n <> 0 by A2, A6, A7, XXREAL_0:2;
(1 / p) * p < p * ((f /" g) . n) by A4, A8, XREAL_1:70;
then 1 < p * ((f /" g) . n) by A4, XCMPLX_1:107;
then A10: 1 < p * ((f . n) / (g . n)) by Lm1;
then A11: 1 < p * ((f . n) * ((g . n) " )) by XCMPLX_0:def 9;
A12: f . n <> 0 by A10;

A13: now

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:12;
then (g (#) (f " )) . n < p * 1 by A12, XCMPLX_0:def 7;
hence ((g /" f) . n) - 0 < p ; :: thesis: verum

end;

A14: now

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:12; :: thesis: verum

end;

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

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

then 1 * (g . n) < ((p * (f . n)) * ((g . n) " )) * (g . n) by A11, XREAL_1:70;
then g . n < (p * (f . n)) * (((g . n) " ) * (g . n)) ;
then A16: g . n < (p * (f . n)) * 1 by A9, XCMPLX_0:def 7;
f . n > 0 by A4, A15, A16;
then (f . n) " > 0 ;
hence abs (((g /" f) . n) - 0 ) < p by A13, A14, A15, A16, ABSVALUE:def 1, XREAL_1:70; :: thesis: verum

end;

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

then 1 * (g . n) > ((p * (f . n)) * ((g . n) " )) * (g . n) by A11, XREAL_1:71;
then g . n > (p * (f . n)) * (((g . n) " ) * (g . n)) ;
then A18: g . n > (p * (f . n)) * 1 by A9, XCMPLX_0:def 7;
A19: f . n < 0 by A4, A17, A18;
(f . n) " < 0 by A19;
hence abs (((g /" f) . n) - 0 ) < p by A13, A14, A17, A18, ABSVALUE:def 1, XREAL_1:71; :: 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