consider n being non zero Nat such that
H: p |^ n = q by defpower;
set E = the SplittingField of X^ ((p |^ n),(PrimeField (Z/ p)));
set F = InducedSubfield (Roots ( the SplittingField of X^ ((p |^ n),(PrimeField (Z/ p))),(X^ ((p |^ n),(PrimeField (Z/ p))))));
A: the carrier of (InducedSubfield (Roots ( the SplittingField of X^ ((p |^ n),(PrimeField (Z/ p))),(X^ ((p |^ n),(PrimeField (Z/ p))))))) = Roots ( the SplittingField of X^ ((p |^ n),(PrimeField (Z/ p))),(X^ ((p |^ n),(PrimeField (Z/ p))))) by dis;
reconsider F = InducedSubfield (Roots ( the SplittingField of X^ ((p |^ n),(PrimeField (Z/ p))),(X^ ((p |^ n),(PrimeField (Z/ p)))))) as finite Field ;
B: order F = q by H, A, lemex;
PrimeField (Z/ p) is Subfield of the SplittingField of X^ ((p |^ n),(PrimeField (Z/ p))) by FIELD_4:7;
then PrimeField (PrimeField (Z/ p)) = PrimeField the SplittingField of X^ ((p |^ n),(PrimeField (Z/ p))) by RING_3:94
.= PrimeField F by RING_3:94 ;
then PrimeField F = PrimeField (Z/ p) by RING_3:95
.= Z/ p by RING_3:110 ;
then reconsider F = F as GaloisField of q by B, defGal;
take F ; :: thesis: F is strict
thus F is strict ; :: thesis: verum