theorem :: NUMBER18:11

for m, n being non zero Nat st m,n are_coprime holds
number_of_divisors (m * n) = (number_of_divisors m) * (number_of_divisors n)