let E be SplittingField of p; :: thesis: E is F -finite
E == FAdj (F,(Roots (E,p))) by XX;
hence E is F -finite by FIELD_7:37; :: thesis: verum