:: deftheorem SqDef defines SqFactors MOEBIUS2:def 3 :
for n being non zero Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = SqFactors n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = p |^ ((p |-count n) div 2) ) ) );