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