let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) <> 0 implies ( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " ) )
set s = f /" g;
set als = abs (lim (f /" g));
set ls = lim (f /" g);
assume that
A1: f /" g is convergent and
A2: lim (f /" g) <> 0 ; :: thesis: ( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " )
consider N1 being Element of NAT such that
A3: for n being Element of NAT st n >= N1 holds
f . n > 0 by Def6;
consider N2 being Element of NAT such that
A4: for n being Element of NAT st n >= N2 holds
g . n > 0 by Def6;
A5: 0 < abs (lim (f /" g)) by A2, COMPLEX1:133;
A6: 0 <> abs (lim (f /" g)) by A2, COMPLEX1:133;
consider n1 being Element of NAT such that
A7: for m being Element of NAT st n1 <= m holds
(abs (lim (f /" g))) / 2 < abs ((f /" g) . m) by A1, A2, SEQ_2:30;
0 * 0 < (abs (lim (f /" g))) * (abs (lim (f /" g))) by A5, XREAL_1:98;
then A8: 0 < ((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2 by XREAL_1:217;

A9: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((g /" f) . m) - ((lim (f /" g)) " )) < p )
assume A10: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((g /" f) . m) - ((lim (f /" g)) " )) < p
then 0 * 0 < p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2) by A8, XREAL_1:98;
then consider n2 being Element of NAT such that
A11: for m being Element of NAT st n2 <= m holds
abs (((f /" g) . m) - (lim (f /" g))) < p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2) by A1, SEQ_2:def 7;
set N3 = N1 + N2;
A12: ( N1 <= N1 + N2 & N2 <= N1 + N2 ) by NAT_1:12;
set N4 = (N1 + N2) + n1;
A13: ( N1 <= (N1 + N2) + n1 & N2 <= (N1 + N2) + n1 & N1 + N2 <= (N1 + N2) + n1 & n1 <= (N1 + N2) + n1 ) by A12, NAT_1:12;
take n = ((N1 + N2) + n1) + n2; :: thesis: for m being Element of NAT st n <= m holds
abs (((g /" f) . m) - ((lim (f /" g)) " )) < p
A14: ( N1 <= n & N2 <= n & N1 + N2 <= n & (N1 + N2) + n1 <= n & n1 <= n & n2 <= n ) by A13, NAT_1:12;
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((g /" f) . m) - ((lim (f /" g)) " )) < p )
assume A15: n <= m ; :: thesis: abs (((g /" f) . m) - ((lim (f /" g)) " )) < p
set asm = abs ((f /" g) . m);
A16: ( N1 <= m & N2 <= m & N1 + N2 <= m & (N1 + N2) + n1 <= m & n1 <= m & n2 <= m ) by A14, A15, XXREAL_0:2;
then A17: abs (((f /" g) . m) - (lim (f /" g))) < p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2) by A11;
A18: (abs (lim (f /" g))) / 2 < abs ((f /" g) . m) by A7, A16;
( f . m <> 0 & g . m <> 0 ) by A3, A4, A16;
then (f . m) / (g . m) <> 0 by XCMPLX_1:50;
then A19: (f /" g) . m <> 0 by Lm1;
then ((f /" g) . m) * (lim (f /" g)) <> 0 by A2, XCMPLX_1:6;
then 0 < abs (((f /" g) . m) * (lim (f /" g))) by COMPLEX1:133;
then 0 < (abs ((f /" g) . m)) * (abs (lim (f /" g))) by COMPLEX1:151;
then A20: (abs (((f /" g) . m) - (lim (f /" g)))) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) < (p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2)) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) by A17, XREAL_1:76;
A21: (p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2)) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) = (p * ((2 " ) * ((abs (lim (f /" g))) * (abs (lim (f /" g)))))) * (((abs ((f /" g) . m)) * (abs (lim (f /" g)))) " ) by XCMPLX_0:def 9
.= (p * (2 " )) * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) * (((abs (lim (f /" g))) * (abs ((f /" g) . m))) " ))
.= (p * (2 " )) * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) * (((abs (lim (f /" g))) " ) * ((abs ((f /" g) . m)) " ))) by XCMPLX_1:205
.= (p * (2 " )) * (((abs (lim (f /" g))) * ((abs (lim (f /" g))) * ((abs (lim (f /" g))) " ))) * ((abs ((f /" g) . m)) " ))
.= (p * (2 " )) * (((abs (lim (f /" g))) * 1) * ((abs ((f /" g) . m)) " )) by A6, XCMPLX_0:def 7
.= (p * ((abs (lim (f /" g))) / 2)) * ((abs ((f /" g) . m)) " )
.= (p * ((abs (lim (f /" g))) / 2)) / (abs ((f /" g) . m)) by XCMPLX_0:def 9 ;
A22: abs (((g /" f) . m) - ((lim (f /" g)) " )) = abs (((g . m) / (f . m)) - ((lim (f /" g)) " )) by Lm1
.= abs ((((f . m) / (g . m)) " ) - ((lim (f /" g)) " )) by XCMPLX_1:215
.= abs ((((f /" g) . m) " ) - ((lim (f /" g)) " )) by Lm1
.= (abs (((f /" g) . m) - (lim (f /" g)))) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) by A2, A19, SEQ_2:11 ;
A23: 0 < (abs (lim (f /" g))) / 2 by A5, XREAL_1:217;
A24: 0 <> (abs (lim (f /" g))) / 2 by A2, COMPLEX1:133;
0 * 0 < p * ((abs (lim (f /" g))) / 2) by A10, A23, XREAL_1:98;
then A25: (p * ((abs (lim (f /" g))) / 2)) / (abs ((f /" g) . m)) < (p * ((abs (lim (f /" g))) / 2)) / ((abs (lim (f /" g))) / 2) by A18, A23, XREAL_1:78;
(p * ((abs (lim (f /" g))) / 2)) / ((abs (lim (f /" g))) / 2) = (p * ((abs (lim (f /" g))) / 2)) * (((abs (lim (f /" g))) / 2) " ) by XCMPLX_0:def 9
.= p * (((abs (lim (f /" g))) / 2) * (((abs (lim (f /" g))) / 2) " ))
.= p * 1 by A24, XCMPLX_0:def 7
.= p ;
hence abs (((g /" f) . m) - ((lim (f /" g)) " )) < p by A20, A21, A22, A25, XXREAL_0:2; :: thesis: verum

end;

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