let t, z be Integer; :: thesis: for a, n being non zero Nat st t mod a = z mod a holds
(t |^ n) mod a = (z |^ n) mod a
let a, n be non zero Nat; :: thesis: ( t mod a = z mod a implies (t |^ n) mod a = (z |^ n) mod a )
assume t mod a = z mod a ; :: thesis: (t |^ n) mod a = (z |^ n) mod a
then t |^ n,z |^ n are_congruent_mod a by NAT_D:64, GR_CY_3:34;
hence (t |^ n) mod a = (z |^ n) mod a by NAT_D:64; :: thesis: verum