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 m being Element of NAT st n1 <= m holds
(abs (lim (f /" g))) / 2 < abs ((f /" g) . m) by A1, A2, SEQ_2:16;
A4: 0 < abs (lim (f /" g)) by A2, COMPLEX1:47;
then 0 * 0 < (abs (lim (f /" g))) * (abs (lim (f /" g))) by XREAL_1:96;
then A5: 0 < ((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2 by XREAL_1:215;
consider N2 being Element of NAT such that
A6: for n being Element of NAT st n >= N2 holds
g . n > 0 by Def6;
consider N1 being Element of NAT such that
A7: for n being Element of NAT st n >= N1 holds
f . n > 0 by Def6;
A8: 0 <> abs (lim (f /" g)) by A2, COMPLEX1:47;

A9: now

set N3 = N1 + N2;
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 )
set N4 = (N1 + N2) + n1;
A10: 0 <> (abs (lim (f /" g))) / 2 by A2, COMPLEX1:47;
A11: (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 A10, XCMPLX_0:def 7
.= p ;
assume A12: 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 A5, XREAL_1:96;
then consider n2 being Element of NAT such that
A13: 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;
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
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((g /" f) . m) - ((lim (f /" g)) ")) < p )
assume A14: n <= m ; :: thesis: abs (((g /" f) . m) - ((lim (f /" g)) ")) < p
set asm = abs ((f /" g) . m);
A15: (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:204
.= (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 A8, 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 ;
n1 <= (N1 + N2) + n1 by NAT_1:12;
then n1 <= n by NAT_1:12;
then n1 <= m by A14, XXREAL_0:2;
then A16: (abs (lim (f /" g))) / 2 < abs ((f /" g) . m) by A3;
A17: 0 < (abs (lim (f /" g))) / 2 by A4, XREAL_1:215;
then 0 * 0 < p * ((abs (lim (f /" g))) / 2) by A12, XREAL_1:96;
then A18: (p * ((abs (lim (f /" g))) / 2)) / (abs ((f /" g) . m)) < (p * ((abs (lim (f /" g))) / 2)) / ((abs (lim (f /" g))) / 2) by A16, A17, XREAL_1:76;
N2 <= N1 + N2 by NAT_1:12;
then N2 <= (N1 + N2) + n1 by NAT_1:12;
then N2 <= n by NAT_1:12;
then N2 <= m by A14, XXREAL_0:2;
then A19: g . m <> 0 by A6;
N1 <= N1 + N2 by NAT_1:12;
then N1 <= (N1 + N2) + n1 by NAT_1:12;
then N1 <= n by NAT_1:12;
then N1 <= m by A14, XXREAL_0:2;
then f . m <> 0 by A7;
then (f . m) / (g . m) <> 0 by A19, XCMPLX_1:50;
then A20: (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:47;
then A21: 0 < (abs ((f /" g) . m)) * (abs (lim (f /" g))) by COMPLEX1:65;
n2 <= n by NAT_1:12;
then n2 <= m by A14, XXREAL_0:2;
then abs (((f /" g) . m) - (lim (f /" g))) < p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2) by A13;
then A22: (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 A21, XREAL_1:74;
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:213
.= 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, A20, SEQ_2:2 ;
hence abs (((g /" f) . m) - ((lim (f /" g)) ")) < p by A22, A15, A18, A11, 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