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

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