theorem Th6: :: NUMBER04:6

for k, n being Nat
for a, b being Integer st k <> 0 & a,b are_congruent_mod n |^ k holds
a,b are_congruent_mod n