let seq be Real_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, SEQ_2:16;
take k = n1; :: thesis: seq ^\ k is non-zero
now :: thesis: for n being Nat holds (seq ^\ k) . n <> 0
let n be Nat; :: thesis: (seq ^\ k) . n <> 0
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 ;
hence (seq ^\ k) . n <> 0 by A4, ABSVALUE:2; :: thesis: verum
end;
hence seq ^\ k is non-zero by SEQ_1:5; :: thesis: verum