let a, b, n be Element of NAT ; :: thesis: (GenFib a,b,n) + (GenFib a,b,(n + 4)) = 3 * (GenFib a,b,(n + 2))
(GenFib a,b,n) + (GenFib a,b,(n + 4)) = (GenFib a,b,n) + ((GenFib a,b,(n + 2)) + (GenFib a,b,(n + 3))) by Th36
.= ((GenFib a,b,n) + (GenFib a,b,(n + 2))) + (GenFib a,b,(n + 3))
.= ((GenFib a,b,n) + (GenFib a,b,(n + 2))) + ((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)) + (GenFib a,b,(n + 2))) + (GenFib a,b,(n + 2)) by Th34
.= 3 * (GenFib a,b,(n + 2)) ;
hence (GenFib a,b,n) + (GenFib a,b,(n + 4)) = 3 * (GenFib a,b,(n + 2)) ; :: thesis: verum