let h be Automorphism of F; :: thesis: h is Z/ p -fixing
order F = p |^ n by defGal;
then { f where f is Automorphism of F : verum } = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) } by FAut;
then h in { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) } ;
then consider m being Nat such that
A: ( h = (Frob F) `^ m & 0 <= m & m <= n - 1 ) ;
thus h is Z/ p -fixing by A; :: thesis: verum