theorem :: FIELD_16:45

for F being finite Field
for a being Element of F holds
( (Frob F) . a = a iff a in PrimeField F )