theorem :: FIB_NUM3:45

for a, n being Element of NAT holds GenFib (a,a,n) = ((GenFib (a,a,0)) / 2) * ((Fib n) + (Lucas n))