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