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 ;
take F ; :: thesis: ( order F = q & Z/ p is Subfield of F )
thus order F = q by H, A, lemex; :: thesis: Z/ p is Subfield of F
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 ;
hence Z/ p is Subfield of F ; :: thesis: verum