theorem :: EULER_1:21

for m, n being Nat st m > 1 & n > 1 & m,n are_coprime holds
Euler (m * n) = (Euler m) * (Euler n)