let a, m be Nat; :: thesis: ( m is prime implies a |^ m,a are_congruent_mod m )
assume A1: m is prime ; :: thesis: a |^ m,a are_congruent_mod m
(a |^ m) mod m = a mod m by A1, ThX;
hence a |^ m,a are_congruent_mod m by A1, NAT_D:64; :: thesis: verum