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