let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq <> 0 & seq is non-zero implies lim (seq ") = (lim seq) " )
assume that
A1: seq is convergent and
A2: lim seq <> 0 and
A3: seq is non-zero ; :: thesis: lim (seq ") = (lim seq) "
A4: seq " is convergent by A1, A2, A3, Th21;
A5: 0 < |.(lim seq).| by A2, COMPLEX1:47;
A6: 0 <> |.(lim seq).| by A2, COMPLEX1:47;
consider n1 being Nat such that
A7: for m being Nat st n1 <= m holds
|.(lim seq).| / 2 < |.(seq . m).| by A1, A2, Th16;
0 * 0 < |.(lim seq).| * |.(lim seq).| by A5;
then A8: 0 < (|.(lim seq).| * |.(lim seq).|) / 2 ;

now :: thesis: for p being Real st 0 < p holds
ex n being set st
for m being Nat st n <= m holds
|.(((seq ") . m) - ((lim seq) ")).| < p

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

end;

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