theorem :: EULER_2:22

for p, k, m being Nat holds (p |^ k) mod m = ((p mod m) |^ k) mod m by Th12P;