let seq be Complex_Sequence; :: thesis: ( seq is convergent & lim seq <> 0 implies ex k being Nat st seq ^\ k is non-zero )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; :: thesis: ex k being Nat st seq ^\ k is non-zero
consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
|.(lim seq).| / 2 < |.(seq . m).| by A1, A2, COMSEQ_2:33;
take k = n1; :: thesis: seq ^\ k is non-zero

now :: thesis: for n being Element of NAT holds (seq ^\ k) . n <> 0c

let n be Element of NAT ; :: thesis: (seq ^\ k) . n <> 0c
0 + k <= n + k by XREAL_1:7;
then |.(lim seq).| / 2 < |.(seq . (n + k)).| by A3;
then A4: |.(lim seq).| / 2 < |.((seq ^\ k) . n).| by NAT_1:def 3;
0 < |.(lim seq).| by A2, COMPLEX1:47;
then 0 / 2 < |.(lim seq).| / 2 by XREAL_1:74;
then 0 < |.((seq ^\ k) . n).| by A4;
hence (seq ^\ k) . n <> 0c by COMPLEX1:47; :: thesis: verum

end;

hence seq ^\ k is non-zero by COMSEQ_1:4; :: thesis: verum