let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
p splits_in FAdj (F,(Roots (E,p)))
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F st p splits_in E holds
p splits_in FAdj (F,(Roots (E,p)))
let E be FieldExtension of F; :: thesis: ( p splits_in E implies p splits_in FAdj (F,(Roots (E,p))) )
assume A: p splits_in E ; :: thesis: p splits_in FAdj (F,(Roots (E,p)))
set K = FAdj (F,(Roots (E,p)));
B: E is FAdj (F,(Roots (E,p))) -extending by FIELD_4:7;
Roots (E,p) is Subset of (FAdj (F,(Roots (E,p)))) by FIELD_6:35;
hence p splits_in FAdj (F,(Roots (E,p))) by A, B, lemma6; :: thesis: verum