let p be Prime; :: thesis: for n being non zero Nat
for F being GaloisField of p |^ n holds F is SplittingField of X^ ((p |^ n),(Z/ p))
let n be non zero Nat; :: thesis: for F being GaloisField of p |^ n holds F is SplittingField of X^ ((p |^ n),(Z/ p))
let F be GaloisField of p |^ n; :: thesis: F is SplittingField of X^ ((p |^ n),(Z/ p))
( order F = p |^ n & PrimeField F = Z/ p ) by PF, defGal;
hence F is SplittingField of X^ ((p |^ n),(Z/ p)) by split; :: thesis: verum