let f be sequence of REAL; :: thesis: ( f is Fibonacci-valued implies f is integer-valued )
assume A1: f is Fibonacci-valued ; :: thesis: f is integer-valued
for x being object st x in dom f holds
f . x is integer

proof

let x be object ; :: thesis: ( x in dom f implies f . x is integer )
assume x in dom f ; :: thesis: f . x is integer
then x in NAT by FUNCT_2:def 1;
then consider fn being Nat such that
A2: ( fn = f . x & fn is Fibonacci ) by A1;
thus f . x is integer by A2; :: thesis: verum

end;

hence f is integer-valued by VALUED_0:def 11; :: thesis: verum