theorem :: INT_4:8

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