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 A1: ( a,b are_congruent_mod n & n <> 0 ) ; :: thesis: a |^ x,b |^ x are_congruent_mod n
( (a |^ x) mod n = ((a mod n) |^ x) mod n & (b |^ x) mod n = ((b mod n) |^ x) mod n ) by PEPIN:12;
then ( (a |^ x) mod n = ((a mod n) |^ x) mod n & (b |^ x) mod n = ((a mod n) |^ x) mod n ) by A1, INT_3:12;
hence a |^ x,b |^ x are_congruent_mod n by INT_3:12, A1; :: thesis: verum