:: deftheorem MySum2Def defines Reci-TSq MOEBIUS3:def 9 :
for b₁ being Real_Sequence holds
( b₁ = Reci-TSq iff ( b₁ . 0 = 0 & ( for i being non zero Nat holds b₁ . i = 1 / (TSqF i) ) ) );