:: deftheorem MyDef defines Reci-seq1 MOEBIUS3:def 2 :
for b₁ being Real_Sequence holds
( b₁ = Reci-seq1 iff for n being Nat holds b₁ . n = 1 / ((n ^2) - (1 / 4)) );