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