theorem GRCY330: :: NEWTON06:80

for a, b being Integer
for n being Nat holds (a |^ n) mod b = ((a mod b) |^ n) mod b