theorem :: INT_4:8

for a, b, m being Nat
for n being Element of NAT st a mod m = b mod m holds
(a |^ n) mod m = (b |^ n) mod m