theorem :: FIB_NUM4:26

for n being Nat holds Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2