let F be finite Field; :: thesis: for a being Element of F holds
( (Frob F) . a = a iff a in PrimeField F )
let a be Element of F; :: thesis: ( (Frob F) . a = a iff a in PrimeField F )
consider p being Prime, n being non zero Nat such that
A: ( Char F = p & order F = p |^ n ) by finex2;
thus ( (Frob F) . a = a iff a in PrimeField F ) by A, Ffix2; :: thesis: verum