theorem Th10: :: INT_8:10

for s, t, i, n being Nat st n > 1 & i,n are_coprime holds
( i |^ s,i |^ t are_congruent_mod n iff s,t are_congruent_mod order (i,n) )