theorem Th23: :: EC_PF_1:23

for n, n1 being Nat
for p being Prime
for a being Element of (GF p) st a = n1 mod p holds
a |^ n = (n1 |^ n) mod p