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:133;
A6: 0 <> abs (lim seq) 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 seq)) / 2 < abs (seq . m) by A1, A2, Th30;
0 * 0 < (abs (lim seq)) * (abs (lim seq)) by A5, XREAL_1:98;
then A8: 0 < ((abs (lim seq)) * (abs (lim seq))) / 2 by XREAL_1:217;

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:98;
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:7;
then (seq . m) * (lim seq) <> 0 by A2, XCMPLX_1:6;
then 0 < abs ((seq . m) * (lim seq)) by COMPLEX1:133;
then 0 < (abs (seq . m)) * (abs (lim seq)) by COMPLEX1:151;
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:76;
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:205
.= (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:217;
A19: 0 <> (abs (lim seq)) / 2 by A2, COMPLEX1:133;
0 * 0 < p * ((abs (lim seq)) / 2) by A9, A18, XREAL_1:98;
then A20: (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) < (p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) by A13, A18, XREAL_1:78;
(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