theorem :: FIB_NUM3:55
for a, n being Element of NAT holds GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1)) = ((2 * a) + 1) * (Fib (n + 2))