:: deftheorem MySumDef defines Reci-Sqf MOEBIUS3:def 8 :
for b₁ being Real_Sequence holds
( b₁ = Reci-Sqf iff ( b₁ . 0 = 0 & ( for i being non zero Nat holds b₁ . i = 1 / (SquarefreePart i) ) ) );