let F be finite Field; :: thesis: for f being Automorphism of F
for a being Element of (PrimeField F) holds f . a = a
let f be Automorphism of F; :: thesis: for a being Element of (PrimeField F) holds f . a = a
let a be Element of (PrimeField F); :: thesis: f . a = a
set P = PrimeField F;
M: the carrier of (PrimeField F) c= the carrier of F by EC_PF_1:def 1;
then reconsider g = f | the carrier of (PrimeField F) as Function of the carrier of (PrimeField F), the carrier of F by FUNCT_2:32;

H: now :: thesis: for o being object st o in the carrier of (PrimeField F) holds
g . o in the carrier of (PrimeField F)

let o be object ; :: thesis: ( o in the carrier of (PrimeField F) implies g . o in the carrier of (PrimeField F) )
assume H1: o in the carrier of (PrimeField F) ; :: thesis: g . o in the carrier of (PrimeField F)
then reconsider a = o as Element of F by M;
a in PrimeField F by H1;
then f . a in PrimeField F by FA4a;
hence g . o in the carrier of (PrimeField F) by H1, FUNCT_1:49; :: thesis: verum

end;

dom g = the carrier of (PrimeField F) by FUNCT_2:def 1;
then reconsider g = g as Function of the carrier of (PrimeField F), the carrier of (PrimeField F) by H, FUNCT_2:3;
A: F is PrimeField F -extending by FIELD_4:7;
B: g is one-to-one by FUNCT_1:52;
card the carrier of (PrimeField F) = card the carrier of (PrimeField F) ;
then g is onto by B, FINSEQ_4:63;
then F: g = id (PrimeField F) by A, PrimAUT;

now :: thesis: for a being Element of (PrimeField F) holds f . a = a

let a be Element of (PrimeField F); :: thesis: f . a = a
thus f . a = g . a by FUNCT_1:49
.= a by F ; :: thesis: verum

end;

hence f . a = a ; :: thesis: verum