ex f being Function of NAT,NAT st
for x being Element of NAT holds f . x = Fib x from FUNCT_2:sch 4();
hence ex b₁ being Function of NAT,NAT st
for k being Element of NAT holds b₁ . k = Fib k ; :: thesis: verum