theorem Th29: :: EC_PF_1:29

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