theorem :: FIB_NUM3:42

for a, b, n being non zero Element of NAT holds GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))