:: deftheorem defines Harmonic MOEBIUS3:def 1 :
for n being Nat holds Harmonic n = (Partial_Sums invNAT) . n;