theorem fresh3: :: FIELD_16:25

for p being Prime
for a being Element of (Z/ p) holds a |^ p = a