theorem Th17: :: NAT_5:17

for k being Nat
for n0, m0 being non zero Nat st n0,m0 are_coprime holds
k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)