let p be Prime; :: thesis: for n being non zero Nat
for F being Field st card F = p |^ n holds
F is SplittingField of X^ ((p |^ n),(PrimeField F))
let n be non zero Nat; :: thesis: for F being Field st card F = p |^ n holds
F is SplittingField of X^ ((p |^ n),(PrimeField F))
let F be Field; :: thesis: ( card F = p |^ n implies F is SplittingField of X^ ((p |^ n),(PrimeField F)) )
assume AS: card F = p |^ n ; :: thesis: F is SplittingField of X^ ((p |^ n),(PrimeField F))
Char F = p by T5, AS;
then ( F is p -characteristic & F is finite ) by AS, RING_3:def 6;
then reconsider U = PrimeField F as finite p -characteristic Field ;
reconsider F = F as FieldExtension of U by FIELD_4:7;
reconsider q = X^ ((p |^ n),(PrimeField F)) as non constant Element of the carrier of (Polynom-Ring U) ;
B: Roots (F,q) = the carrier of F

proof

H: Roots (F,q) = { a where a is Element of F : a is_a_root_of q,F } by FIELD_4:def 4;

now :: thesis: for o being object st o in the carrier of F holds
o in Roots (F,q)

let o be object ; :: thesis: ( o in the carrier of F implies o in Roots (F,q) )
assume o in the carrier of F ; :: thesis: o in Roots (F,q)
then reconsider a = o as Element of F ;
Ext_eval ((X^ ((p |^ n),U)),a) = 0. F by AS, thX1e;
then a is_a_root_of q,F by FIELD_4:def 2;
hence o in Roots (F,q) by H; :: thesis: verum

end;

then the carrier of F c= Roots (F,q) ;
hence Roots (F,q) = the carrier of F by XBOOLE_0:def 10; :: thesis: verum

end;

then D: card (Roots (F,q)) = deg q by AS, Lm12;
then C: q splits_in F by lemMA;

now :: thesis: for E being FieldExtension of U st q splits_in E & E is Subfield of F holds
E == F

let E be FieldExtension of U; :: thesis: ( q splits_in E & E is Subfield of F implies E == F )
assume D: ( q splits_in E & E is Subfield of F ) ; :: thesis: E == F
then F is E -extending FieldExtension of U by FIELD_4:7;
then E: Roots (F,q) c= Roots (E,q) by C, D, FIELD_8:28;
Roots (E,q) c= the carrier of E ;
then F: the carrier of F c= the carrier of E by B, E;
the carrier of E c= the carrier of F by D, EC_PF_1:def 1;
then G: the carrier of F = the carrier of E by F, XBOOLE_0:def 10;
( the addF of E = the addF of F || the carrier of E & the multF of E = the multF of F || the carrier of E & 1. E = 1. F & 0. E = 0. F ) by D, EC_PF_1:def 1;
hence E == F by G; :: thesis: verum

end;

hence F is SplittingField of X^ ((p |^ n),(PrimeField F)) by lemMA, D, FIELD_8:def 1; :: thesis: verum