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