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

(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