take f = seq_const 0; :: thesis: f is Fibonacci-valued
for n being Nat ex fn being Nat st
( fn = f . n & fn is Fibonacci )

proof

let n be Nat; :: thesis: ex fn being Nat st
( fn = f . n & fn is Fibonacci )
take f . n ; :: thesis: ( f . n = f . n & f . n is Fibonacci )
thus ( f . n = f . n & f . n is Fibonacci ) by PRE_FF:1; :: thesis: verum

end;

hence f is Fibonacci-valued ; :: thesis: verum