let a, b be Nat; :: thesis: for n being Nat holds a |^ n,(a - b) |^ n are_congruent_mod b
for n being Nat holds b divides (((a - b) + b) |^ n) - ((a - b) |^ n) by NEWTON02:10;
hence for n being Nat holds a |^ n,(a - b) |^ n are_congruent_mod b ; :: thesis: verum