for t, z being Integer
for a, n being non zero Nat st t mod a = z mod a holds
(t |^ n) mod a = (z |^ n) mod a