theorem :: PEPIN:12

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