theorem FA4: :: FIELD_16:49

for F being finite Field
for f being Automorphism of F
for a being Element of (PrimeField F) holds f . a = a