Harmonic 0 = invNAT . 0 by SERIES_1:def 1
.= 1 / 0 by MOEBIUS2:def 2
.= 0 ;
hence Harmonic 0 = 0 ; :: thesis: verum