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

now

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

end;

hence seq ^\ k is non-zero by SEQ_1:7; :: thesis: verum