:: deftheorem ReciPr defines ReciPrime MOEBIUS2:def 1 :
for b₁ being Real_Sequence holds
( b₁ = ReciPrime iff for i being Nat holds b₁ . i = 1 / (primenumber i) );