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