let s be Complex_Sequence; :: thesis: ( s is convergent & lim s <> 0c & s is non-zero implies lim (s " ) = (lim s) " )
assume that
A1: s is convergent and
A2: lim s <> 0c and
A3: s is non-zero ; :: thesis: lim (s " ) = (lim s) "
A4: s " is convergent by A1, A2, A3, Th34;
A5: 0 < |.(lim s).| by A2, COMPLEX1:133;
A6: 0 <> |.(lim s).| by A2, COMPLEX1:133;
consider n1 being Element of NAT such that
A7: for m being Element of NAT st n1 <= m holds
|.(lim s).| / 2 < |.(s . m).| by A1, A2, Th33;
0 * 0 < |.(lim s).| * |.(lim s).| by A5, XREAL_1:98;
then A8: 0 < (|.(lim s).| * |.(lim s).|) / 2 by XREAL_1:217;

now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s " ) . m) - ((lim s) " )).| < p )
assume A9: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s " ) . m) - ((lim s) " )).| < p
then 0 * 0 < p * ((|.(lim s).| * |.(lim s).|) / 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
|.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A1, Def5;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
|.(((s " ) . m) - ((lim s) " )).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s " ) . m) - ((lim s) " )).| < p )
assume A11: n <= m ; :: thesis: |.(((s " ) . m) - ((lim s) " )).| < p
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A12: |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A10;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A13: |.(lim s).| / 2 < |.(s . m).| by A7;
A14: s . m <> 0c by A3, COMSEQ_1:3;
then (s . m) * (lim s) <> 0c by A2, XCMPLX_1:6;
then 0 < |.((s . m) * (lim s)).| by COMPLEX1:133;
then 0 < |.(s . m).| * |.(lim s).| by COMPLEX1:151;
then A15: |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) < (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) by A12, XREAL_1:76;
A16: (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:205
.= (p * (2 " )) * ((|.(lim s).| * (|.(lim s).| * (|.(lim s).| " ))) * (|.(s . m).| " ))
.= (p * (2 " )) * ((|.(lim s).| * 1) * (|.(s . m).| " )) by A6, XCMPLX_0:def 7
.= (p * (|.(lim s).| / 2)) * (|.(s . m).| " )
.= (p * (|.(lim s).| / 2)) / |.(s . m).| by XCMPLX_0:def 9 ;
A17: |.(((s " ) . m) - ((lim s) " )).| = |.(((s . m) " ) - ((lim s) " )).| by VALUED_1:10
.= |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) by A2, A14, Th1 ;
A18: 0 < |.(lim s).| / 2 by A5, XREAL_1:217;
A19: 0 <> |.(lim s).| / 2 by A2, COMPLEX1:133;
0 * 0 < p * (|.(lim s).| / 2) by A9, A18, XREAL_1:98;
then A20: (p * (|.(lim s).| / 2)) / |.(s . m).| < (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) by A13, A18, XREAL_1:78;
(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 A19, XCMPLX_0:def 7
.= p ;
hence |.(((s " ) . m) - ((lim s) " )).| < p by A15, A16, A17, A20, XXREAL_0:2; :: thesis: verum

end;

hence lim (s " ) = (lim s) " by A4, Def5; :: thesis: verum