theorem Th17: :: INT_8:17

for s, t, n being Nat st n > 1 & s,n are_coprime & t,n are_coprime & order (s,n), order (t,n) are_coprime holds
order ((s * t),n) = (order (s,n)) * (order (t,n))