for t being Integer
for n being odd Nat holds (t |^ n) mod 3 = t mod 3