let f be Real_Sequence; :: thesis: ( f is non-zero & f is constant implies f is eventually-non-zero )

assume A0: ( f is non-zero & f is constant ) ; :: thesis: f is eventually-non-zero

consider x being set such that

A1: ( x in dom f & the_value_of f = f . x ) by FUNCT_1:def 12, A0;

A2: the_value_of f in rng f by A1, FUNCT_1:3;

reconsider v = the_value_of f as Real by A1;

A3: dom f = NAT by FUNCT_2:def 1;

let n be Nat; :: according to LIOUVIL1:def 3 :: thesis: ex N being Nat st

( n <= N & f . N <> 0 )

take N = n + 1; :: thesis: ( n <= N & f . N <> 0 )

thus ( n <= N & f . N <> 0 ) by A0, A1, A2, A3, XREAL_1:31, FUNCT_1:def 10; :: thesis: verum

assume A0: ( f is non-zero & f is constant ) ; :: thesis: f is eventually-non-zero

consider x being set such that

A1: ( x in dom f & the_value_of f = f . x ) by FUNCT_1:def 12, A0;

A2: the_value_of f in rng f by A1, FUNCT_1:3;

reconsider v = the_value_of f as Real by A1;

A3: dom f = NAT by FUNCT_2:def 1;

let n be Nat; :: according to LIOUVIL1:def 3 :: thesis: ex N being Nat st

( n <= N & f . N <> 0 )

take N = n + 1; :: thesis: ( n <= N & f . N <> 0 )

thus ( n <= N & f . N <> 0 ) by A0, A1, A2, A3, XREAL_1:31, FUNCT_1:def 10; :: thesis: verum