for p being Prime
for x being Element of (MultGroup (GF p))
for x1 being Element of (GF p)
for n being Nat st x = x1 holds
x |^ n = x1 |^ n