theorem :: INT_8:15

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