let a, b, n be Element of NAT ; :: thesis: (GenFib a,b,(n + 3)) - (GenFib a,b,n) = 2 * (GenFib a,b,(n + 1))
(GenFib a,b,(n + 3)) - (GenFib a,b,n) = ((GenFib a,b,(n + 1)) + (GenFib a,b,(n + 2))) - (GenFib a,b,n) by Th35
.= ((GenFib a,b,(n + 1)) + ((GenFib a,b,n) + (GenFib a,b,(n + 1)))) - (GenFib a,b,n) by Th34
.= 2 * (GenFib a,b,(n + 1)) ;
hence (GenFib a,b,(n + 3)) - (GenFib a,b,n) = 2 * (GenFib a,b,(n + 1)) ; :: thesis: verum