:: deftheorem Def5 defines SMoebius MOEBIUS1:def 5 :
for X being set
for b₂ being ManySortedSet of NAT holds
( b₂ = SMoebius X iff ( support b₂ = X /\ SCNAT & ( for k being Nat st k in support b₂ holds
b₂ . k = Moebius k ) ) );