let s be convergent Complex_Sequence; :: thesis: ( lim s <> 0c & s is non-zero implies s " is convergent )
assume that
A1: lim s <> 0c and
A2: s is non-zero ; :: thesis: s " is convergent
consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
|.(lim s).| / 2 < |.(s . m).| by A1, Th22;
take (lim s) " ; :: according to COMSEQ_2:def 5 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p )
assume A4: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p
A5: 0 < |.(lim s).| by A1, COMPLEX1:47;
then 0 * 0 < |.(lim s).| * |.(lim s).| ;
then 0 < (|.(lim s).| * |.(lim s).|) / 2 ;
then 0 * 0 < p * ((|.(lim s).| * |.(lim s).|) / 2) by A4;
then consider n2 being Nat such that
A6: for m being Nat st n2 <= m holds
|.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by Def6;
take n = n1 + n2; :: thesis: for m being Nat st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((s ") . m) - ((lim s) ")).| < p )
assume A7: n <= m ; :: thesis: |.(((s ") . m) - ((lim s) ")).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A7, XXREAL_0:2;
then A8: |.(lim s).| / 2 < |.(s . m).| by A3;
A9: 0 < |.(lim s).| / 2 by A5;
then 0 * 0 < p * (|.(lim s).| / 2) by A4;
then A10: (p * (|.(lim s).| / 2)) / |.(s . m).| < (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) by A8, A9, XREAL_1:76;
A11: 0 <> |.(lim s).| / 2 by A1, COMPLEX1:47;
A12: (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) = (p * (|.(lim s).| / 2)) * ((|.(lim s).| / 2) ") by XCMPLX_0:def 9
.= p * ((|.(lim s).| / 2) * ((|.(lim s).| / 2) "))
.= p * 1 by A11, XCMPLX_0:def 7
.= p ;
A13: 0 <> |.(lim s).| by A1, COMPLEX1:47;
A14: (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) = (p * ((2 ") * (|.(lim s).| * |.(lim s).|))) * ((|.(s . m).| * |.(lim s).|) ") by XCMPLX_0:def 9
.= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| * |.(s . m).|) "))
.= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| ") * (|.(s . m).| "))) by XCMPLX_1:204
.= (p * (2 ")) * ((|.(lim s).| * (|.(lim s).| * (|.(lim s).| "))) * (|.(s . m).| "))
.= (p * (2 ")) * ((|.(lim s).| * 1) * (|.(s . m).| ")) by A13, XCMPLX_0:def 7
.= (p * (|.(lim s).| / 2)) * (|.(s . m).| ")
.= (p * (|.(lim s).| / 2)) / |.(s . m).| by XCMPLX_0:def 9 ;
m in NAT by ORDINAL1:def 12;
then A15: s . m <> 0 by A2, COMSEQ_1:3;
then (s . m) * (lim s) <> 0c by A1;
then 0 < |.((s . m) * (lim s)).| by COMPLEX1:47;
then A16: 0 < |.(s . m).| * |.(lim s).| by COMPLEX1:65;
n2 <= n by NAT_1:12;
then n2 <= m by A7, XXREAL_0:2;
then |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A6;
then A17: |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) < (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) by A16, XREAL_1:74;
|.(((s ") . m) - ((lim s) ")).| = |.(((s . m) ") - ((lim s) ")).| by VALUED_1:10
.= |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) by A1, Th1, A15 ;
hence |.(((s ") . m) - ((lim s) ")).| < p by A17, A14, A10, A12, XXREAL_0:2; :: thesis: verum