( order F = p |^ n & PrimeField F = Z/ p ) by PF, defGal;
hence (Frob F) `^ m is Z/ p -fixing by FA4; :: thesis: verum