:: deftheorem DefRec defines invNAT MOEBIUS2:def 2 :
for b₁ being Real_Sequence holds
( b₁ = invNAT iff for i being Nat holds b₁ . i = 1 / i );