let F be finite Field; :: thesis: for f being Automorphism of F
for a being Element of F holds
( f . a in PrimeField F iff a in PrimeField F )
let f be Automorphism of F; :: thesis: for a being Element of F holds
( f . a in PrimeField F iff a in PrimeField F )
let a be Element of F; :: thesis: ( f . a in PrimeField F iff a in PrimeField F )
consider n being non zero Nat such that
AS: card F = (Char F) |^ n by FIELD_15:92;
set p = Char F;
set P = PrimeField F;
reconsider F = F as Char F -characteristic Field by RING_3:def 6;
id F is isomorphism ;
then H: F is F -homomorphic Ring by RING_2:def 4;

A: now :: thesis: ( f . a in PrimeField F implies a in PrimeField F )

assume f . a in PrimeField F ; :: thesis: a in PrimeField F
then f . a = (f . a) |^ (Char F) by AS, fresh3P
.= f . (a |^ (Char F)) by H, lemID ;
then a = a |^ (Char F) by FUNCT_2:19;
hence a in PrimeField F by AS, fresh3P; :: thesis: verum

end;

now :: thesis: ( a in PrimeField F implies f . a in PrimeField F )

assume a in PrimeField F ; :: thesis: f . a in PrimeField F
then a = a |^ (Char F) by AS, fresh3P;
then f . a = (f . a) |^ (Char F) by H, lemID;
hence f . a in PrimeField F by AS, fresh3P; :: thesis: verum

end;

hence ( f . a in PrimeField F iff a in PrimeField F ) by A; :: thesis: verum