:: deftheorem Def6 defines PFactors MOEBIUS1:def 6 :
for n being non zero Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = PFactors n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = p ) ) );