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