let a, n be Element of NAT ; :: thesis: GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1)) = ((2 * a) + 1) * (Fib (n + 2))
GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1)) = (((2 * a) + 1) * (Fib n)) + (((2 * a) + 1) * (Fib (n + 1))) by Th49
.= ((2 * a) + 1) * ((Fib n) + (Fib (n + 1)))
.= ((2 * a) + 1) * (Fib (n + 2)) by FIB_NUM2:24 ;
hence GenFib (((2 * a) + 1),((2 * a) + 1),(n + 1)) = ((2 * a) + 1) * (Fib (n + 2)) ; :: thesis: verum