let F be prime Field; :: thesis: for f being Automorphism of F holds f = id F
let f be Automorphism of F; :: thesis: f = id F
A: F = PrimeField F by RING_3:96;

per cases ( Char F = 0 or Char F is prime ) by RING_3:86;

suppose Char F = 0 ; :: thesis: f = id F

then F, F_Rat are_isomorphic by A, RING_3:113;
then consider h being Function of F,F_Rat such that
B: h is isomorphism ;
reconsider FRat = F_Rat as F -isomorphic Field by B, RING_3:def 4;
reconsider h = h as Isomorphism of F,FRat by B;
reconsider g2 = h " as Isomorphism of FRat,F by RING_3:73;
g2 is isomorphism ;
then reconsider F = F as FRat -isomorphic Field by RING_3:def 4;
D: rng h = the carrier of FRat by FUNCT_2:def 3;
reconsider g1 = f * g2 as Function of FRat,F ;
reconsider g = h * (f * g2) as Function of FRat,FRat ;
E: g1 is isomorphism ;
(h ") * g = ((h ") * h) * (f * (h ")) by T2
.= (id F) * (f * (h ")) by D, FUNCT_2:29
.= f * (h ") ;
then ((h ") * g) * h = f * ((h ") * h) by T2
.= f * (id F) by D, FUNCT_2:29
.= f ;
then f = ((h ") * (id FRat)) * h by E, RING_3:100
.= id F by D, FUNCT_2:29 ;
hence f = id F ; :: thesis: verum

end;

suppose Char F is prime ; :: thesis: f = id F

then reconsider p = Char F as Prime ;
F, Z/ p are_isomorphic by A, RING_3:114;
then consider h being Function of F,(Z/ p) such that
B: h is isomorphism ;
reconsider Zp = Z/ p as F -isomorphic Field by B, RING_3:def 4;
reconsider h = h as Isomorphism of F,Zp by B;
reconsider g2 = h " as Isomorphism of Zp,F by RING_3:73;
g2 is isomorphism ;
then reconsider F = F as Zp -isomorphic Field by RING_3:def 4;
D: rng h = the carrier of Zp by FUNCT_2:def 3;
reconsider g1 = f * g2 as Function of Zp,F ;
reconsider g = h * (f * g2) as Function of Zp,Zp ;
E: g1 is isomorphism ;
(h ") * g = ((h ") * h) * (f * (h ")) by T2
.= (id F) * (f * (h ")) by D, FUNCT_2:29
.= f * (h ") ;
then ((h ") * g) * h = f * ((h ") * h) by T2
.= f * (id F) by D, FUNCT_2:29
.= f ;
then f = ((h ") * (id (Z/ p))) * h by E, RING_3:107
.= id F by D, FUNCT_2:29 ;
hence f = id F ; :: thesis: verum

end;

end;