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

now

let n be Element of NAT ; :: thesis: (seq ^\ k) . n <> 0c
0 <= n by NAT_1:2;
then 0 + k <= n + k by XREAL_1:9;
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:133;
then 0 / 2 < |.(lim seq).| / 2 by XREAL_1:76;
then 0 < |.((seq ^\ k) . n).| by A4, XXREAL_0:2;
hence (seq ^\ k) . n <> 0c by COMPLEX1:133; :: thesis: verum

end;

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