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