theorem Th40: :: FIB_NUM2:40

for n being Nat
for k being non zero Element of NAT holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))