:: deftheorem My3Def defines Reci-seq2 MOEBIUS3:def 3 :
for b₁ being Real_Sequence holds
( b₁ = Reci-seq2 iff for n being Nat holds b₁ . n = 1 + (1 / (primenumber n)) );