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