theorem :: NUMBER18:16

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