theorem Harmon1: :: MOEBIUS3:9

for n being Nat holds Harmonic (n + 1) = (Harmonic n) + (1 / (n + 1))