:: deftheorem Def9 defines prime_factorization NAT_3:def 9 :
for n being non zero Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = prime_factorization n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = p |^ (p |-count n) ) ) );