theorem :: FIB_NUM3:31

for n being Element of NAT holds Fib ((2 * n) + 1) = ((Fib (n + 1)) * (Lucas (n + 1))) - ((Fib n) * (Lucas n))