theorem Th35: :: MOEBIUS1:35

for m, n being non zero Element of NAT st m,n are_coprime holds
Moebius (m * n) = (Moebius m) * (Moebius n)