for F being Real_Sequence st ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) holds
( F is convergent & lim F = tau )