for a, b, c being Nat holds (a |^ (2 * b)) mod c = (((a |^ b) mod c) * ((a |^ b) mod c)) mod c