theorem :: NUMBER18:1

for p being Prime holds (Bnumber_of_divisors p) * <*p*> = <*2*>