:: deftheorem defines Compose MOEBIUS3:def 10 :
for n being non zero Nat
for b₂ being Function of [:(bool (SetPrimes n)),(Seg n):],NAT holds
( b₂ = Compose n iff for x being Element of [:(bool (SetPrimes n)),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
b₂ . x = (Product ((A,1) -bag)) * (k ^2) );