theorem Th30: :: GR_CY_3:30

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