let f be Real_Sequence; :: thesis: ( f is eventually-nonzero implies f is eventually-non-zero )
assume A1: f is eventually-nonzero ; :: thesis: f is eventually-non-zero
let n be Nat; :: according to LIOUVIL1:def 3 :: thesis: ex N being Nat st
( n <= N & f . N <> 0 )
consider N being Nat such that
A2: for k being Nat st k >= N holds
f . k <> 0 by A1;
reconsider m = max (N,n) as Nat ;
f . m <> 0 by A2, XXREAL_0:25;
hence ex N being Nat st
( n <= N & f . N <> 0 ) by XXREAL_0:25; :: thesis: verum