theorem :: GR_CY_3:34

for a, b being Integer
for n, x being Nat st a,b are_congruent_mod n & n <> 0 holds
a |^ x,b |^ x are_congruent_mod n