:: deftheorem defines number_of_divisors NUMBER18:def 2 :
for n being non zero Nat holds number_of_divisors n = Product (Bnumber_of_divisors n);