let a, b, n, x be Nat; :: thesis: ( a,b are_congruent_mod n & n <> 0 implies a |^ x,b |^ x are_congruent_mod n )
assume that
A1: a,b are_congruent_mod n and
A2: n <> 0 ; :: thesis: a |^ x,b |^ x are_congruent_mod n
A3: (a |^ x) mod n = ((a mod n) |^ x) mod n by PEPIN:12;
(b |^ x) mod n = ((b mod n) |^ x) mod n by PEPIN:12;
then (b |^ x) mod n = ((a mod n) |^ x) mod n by A1, NAT_D:64;
hence a |^ x,b |^ x are_congruent_mod n by A2, A3, NAT_D:64; :: thesis: verum