:: deftheorem Def3 defines Moebius MOEBIUS1:def 3 :
for n being Nat
for b₂ being Real holds
( ( n is square-containing implies ( b₂ = Moebius n iff b₂ = 0 ) ) & ( not n is square-containing implies ( b₂ = Moebius n iff ex n9 being non zero Nat st
( n9 = n & b₂ = (- 1) |^ (card (support (ppf n9))) ) ) ) );