reconsider p1 = p as Polynomial of F ;
p splits_in E by FIELD_8:def 1;
then consider a being non zero Element of E, q being Ppoly of E such that
A: p = a * q by FIELD_4:def 5;
a * q is Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
then Roots (E,p) = Roots (a * q) by A, FIELD_7:13;
hence not Roots (E,p) is empty ; :: thesis: verum