let p be Prime; :: thesis: for n being non zero Nat
for F being p -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = p |^ n
let n be non zero Nat; :: thesis: for F being p -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = p |^ n
let F be p -characteristic Field; :: thesis: for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = p |^ n
let E be SplittingField of X^ ((p |^ n),(PrimeField F)); :: thesis: card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = p |^ n
X^ ((p |^ n),(PrimeField F)) splits_in E by FIELD_8:def 1;
then card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = deg (X^ ((p |^ n),(PrimeField F))) by lemMA;
hence card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = p |^ n by Lm12; :: thesis: verum