let a, b be Integer; :: thesis: for n being Nat holds (a |^ n) mod b = ((a mod b) |^ n) mod b
let n be Nat; :: thesis: (a |^ n) mod b = ((a mod b) |^ n) mod b
a mod b = (a mod b) mod b ;
hence (a |^ n) mod b = ((a mod b) |^ n) mod b by INT_5:13; :: thesis: verum