let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for E being SplittingField of p holds E == FAdj (F,(Roots (E,p)))
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for E being SplittingField of p holds E == FAdj (F,(Roots (E,p)))
let E be SplittingField of p; :: thesis: E == FAdj (F,(Roots (E,p)))
set K = FAdj (F,(Roots (E,p)));
p splits_in E by defspl;
then FAdj (F,(Roots (E,p))) is SplittingField of p by spl1;
then p splits_in FAdj (F,(Roots (E,p))) by defspl;
hence E == FAdj (F,(Roots (E,p))) by defspl; :: thesis: verum