let n be Nat; :: thesis: Harmonic (n + 1) = (Harmonic n) + (1 / (n + 1))
(Partial_Sums invNAT) . (n + 1) = ((Partial_Sums invNAT) . n) + (invNAT . (n + 1)) by SERIES_1:def 1
.= (Harmonic n) + (1 / (n + 1)) by MOEBIUS2:def 2 ;
hence Harmonic (n + 1) = (Harmonic n) + (1 / (n + 1)) ; :: thesis: verum