let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq <> 0 & seq is non-empty implies lim (seq ") = (lim seq) " )
assume that
A1: seq is convergent and
A2: lim seq <> 0 and
A3: seq is non-empty ; :: thesis: lim (seq ") = (lim seq) "
A4: seq " is convergent by A1, A2, A3, Th35;
A5: 0 < abs (lim seq) by A2, COMPLEX1:47;
A6: 0 <> abs (lim seq) by A2, COMPLEX1:47;
consider n1 being Element of NAT such that
A7: for m being Element of NAT st n1 <= m holds
(abs (lim seq)) / 2 < abs (seq . m) by A1, A2, Th30;
0 * 0 < (abs (lim seq)) * (abs (lim seq)) by A5, XREAL_1:96;
then A8: 0 < ((abs (lim seq)) * (abs (lim seq))) / 2 by XREAL_1:215;

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 (((seq ") . m) - ((lim seq) ")) < p )
assume A9: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
then 0 * 0 < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A8, XREAL_1:96;
then consider n2 being Element of NAT such that
A10: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A1, Def7;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((seq ") . m) - ((lim seq) ")) < p )
assume A11: n <= m ; :: thesis: abs (((seq ") . m) - ((lim seq) ")) < p
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A12: abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A10;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A13: (abs (lim seq)) / 2 < abs (seq . m) by A7;
A14: seq . m <> 0 by A3, SEQ_1:5;
then (seq . m) * (lim seq) <> 0 by A2, XCMPLX_1:6;
then 0 < abs ((seq . m) * (lim seq)) by COMPLEX1:47;
then 0 < (abs (seq . m)) * (abs (lim seq)) by COMPLEX1:65;
then A15: (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) < (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) by A12, XREAL_1:74;
A16: (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) = (p * ((2 ") * ((abs (lim seq)) * (abs (lim seq))))) * (((abs (seq . m)) * (abs (lim seq))) ") by XCMPLX_0:def 9
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) * (abs (seq . m))) "))
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) ") * ((abs (seq . m)) "))) by XCMPLX_1:204
.= (p * (2 ")) * (((abs (lim seq)) * ((abs (lim seq)) * ((abs (lim seq)) "))) * ((abs (seq . m)) "))
.= (p * (2 ")) * (((abs (lim seq)) * 1) * ((abs (seq . m)) ")) by A6, XCMPLX_0:def 7
.= (p * ((abs (lim seq)) / 2)) * ((abs (seq . m)) ")
.= (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) by XCMPLX_0:def 9 ;
A17: abs (((seq ") . m) - ((lim seq) ")) = abs (((seq . m) ") - ((lim seq) ")) by VALUED_1:10
.= (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) by A2, A14, Th11 ;
A18: 0 < (abs (lim seq)) / 2 by A5, XREAL_1:215;
A19: 0 <> (abs (lim seq)) / 2 by A2, COMPLEX1:47;
0 * 0 < p * ((abs (lim seq)) / 2) by A9, A18, XREAL_1:96;
then A20: (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) < (p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) by A13, A18, XREAL_1:76;
(p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) = (p * ((abs (lim seq)) / 2)) * (((abs (lim seq)) / 2) ") by XCMPLX_0:def 9
.= p * (((abs (lim seq)) / 2) * (((abs (lim seq)) / 2) "))
.= p * 1 by A19, XCMPLX_0:def 7
.= p ;
hence abs (((seq ") . m) - ((lim seq) ")) < p by A15, A16, A17, A20, XXREAL_0:2; :: thesis: verum

end;

hence lim (seq ") = (lim seq) " by A4, Def7; :: thesis: verum