:: deftheorem Def8 defines prime_exponents NAT_3:def 8 :
for n being Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = prime_exponents n iff for p being Prime holds b₂ . p = p |-count n );