let p be Prime; :: thesis: for n being non zero Nat
for F being Field st card F = p |^ n holds
{ f where f is Automorphism of F : verum } = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) }
let n be non zero Nat; :: thesis: for F being Field st card F = p |^ n holds
{ f where f is Automorphism of F : verum } = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) }
let F be Field; :: thesis: ( card F = p |^ n implies { f where f is Automorphism of F : verum } = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) } )
assume AS1: card F = p |^ n ; :: thesis: { f where f is Automorphism of F : verum } = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) }
then AS2: F is finite ;
set P = PrimeField F;
reconsider E = F as PrimeField F -finite FieldExtension of PrimeField F by AS2, FA1;
consider a being Element of E such that
A: E == FAdj ((PrimeField F),{a}) by AS2, FIELD_14:def 7;
set M = { f where f is PrimeField F -fixing Automorphism of (FAdj ((PrimeField F),{a})) : verum } ;
reconsider M = { f where f is PrimeField F -fixing Automorphism of (FAdj ((PrimeField F),{a})) : verum } as finite set by FAUTfin;
C: card { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) } = n by AS1, Frobcard;
then reconsider K = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) } as finite set ;
set m = card M;
C1: deg ((FAdj ((PrimeField F),{a})),(PrimeField F)) = deg (E,(PrimeField F)) by A, FIELD_7:5
.= n by AS1, FA3 ;
C2: card M <= card (Roots ((FAdj ((PrimeField F),{a})),(MinPoly (a,(PrimeField F))))) by FAUTh;
C3: card (Roots ((FAdj ((PrimeField F),{a})),(MinPoly (a,(PrimeField F))))) <= deg (MinPoly (a,(PrimeField F))) by ID2;
deg (MinPoly (a,(PrimeField F))) = n by C1, FIELD_6:67;
then D: card M <= n by C2, C3, XXREAL_0:2;
E: M = { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum }

proof

E1: now :: thesis: for o being object st o in { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum } holds
o in M

let o be object ; :: thesis: ( o in { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum } implies o in M )
assume o in { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum } ; :: thesis: o in M
then consider f being Automorphism of (FAdj ((PrimeField F),{a})) such that
E2: o = f ;
PrimeField (FAdj ((PrimeField F),{a})) = PrimeField F by RING_3:94;
then f is PrimeField F -fixing by AS2, FA4;
hence o in M by E2; :: thesis: verum

end;

now :: thesis: for o being object st o in M holds
o in { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum }

let o be object ; :: thesis: ( o in M implies o in { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum } )
assume o in M ; :: thesis: o in { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum }
then consider f being PrimeField F -fixing Automorphism of (FAdj ((PrimeField F),{a})) such that
E3: o = f ;
thus o in { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum } by E3; :: thesis: verum

end;

hence M = { f where f is Automorphism of (FAdj ((PrimeField F),{a})) : verum } by E1, TARSKI:2; :: thesis: verum

end;

B: K c= M

proof

now :: thesis: for o being object st o in K holds
o in M

let o be object ; :: thesis: ( o in K implies o in M )
assume o in K ; :: thesis: o in M
then consider m being Nat such that
B1: ( o = (Frob F) `^ m & 0 <= m & m <= n - 1 ) ;
reconsider f = (Frob F) `^ m as Automorphism of (FAdj ((PrimeField F),{a})) by AS2, A, FAutEQ1;
f is PrimeField F -fixing by AS2, FA4;
hence o in M by B1; :: thesis: verum

end;

hence K c= M ; :: thesis: verum

end;

then n <= card M by C, NAT_1:43;
then K = M by B, C, D, XXREAL_0:1, FIELD_10:4;
hence { f where f is Automorphism of F : verum } = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) } by E, A, FAutEQ; :: thesis: verum