let f be eventually-non-zero Real_Sequence; :: thesis: for n being Nat holds f ^\ n is eventually-non-zero
let n be Nat; :: thesis: f ^\ n is eventually-non-zero
set g = f ^\ n;
let k be Nat; :: according to LIOUVIL1:def 3 :: thesis: ex N being Nat st
( k <= N & (f ^\ n) . N <> 0 )
consider N being Nat such that
A1: ( k + n <= N & f . N <> 0 ) by ENZ;
k <= N - n by A1, XREAL_1:19;
then N - n in NAT by INT_1:3;
then reconsider Nn = N - n as Nat ;
take Nn ; :: thesis: ( k <= Nn & (f ^\ n) . Nn <> 0 )
(f ^\ n) . Nn = f . (Nn + n) by NAT_1:def 3
.= f . N ;
hence ( k <= Nn & (f ^\ n) . Nn <> 0 ) by A1, XREAL_1:19; :: thesis: verum