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