let p be Prime; :: thesis: for n being non zero Nat ex F being finite Field st
( Char F = p & order F = p |^ n )
let n be non zero Nat; :: thesis: ex F being finite Field st
( Char F = p & order F = p |^ n )
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: ( Char F = p & order F = p |^ n )
thus Char F = p by RING_3:def 6; :: thesis: order F = p |^ n
thus order F = p |^ n by A, lemex; :: thesis: verum