:: deftheorem BDef defines Bnumber_of_divisors NUMBER18:def 1 :
for n being Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = Bnumber_of_divisors n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = (p |-count n) + 1 ) ) );