let F be polynomial_disjoint Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f is_with_roots_in E
let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st f is_with_roots_in E
consider p being Element of the carrier of (Polynom-Ring F) such that
A1: p is_a_irreducible_factor_of f by FIELD_1:3;
reconsider p = p as irreducible Element of the carrier of (Polynom-Ring F) by A1, FIELD_1:def 1;
consider q being Element of the carrier of (Polynom-Ring F) such that
A2: p * q = f by A1, FIELD_1:def 1, GCD_1:def 1;
consider E being FieldExtension of F such that
A3: p is_with_roots_in E by Lm11;
take E ; :: thesis: f is_with_roots_in E
consider a being Element of E such that
A4: a is_a_root_of p,E by A3;
reconsider p1 = p, q1 = q as Polynomial of F ;
A5: F is Subring of E by Def1;
Ext_eval (f,a) = Ext_eval ((p1 *' q1),a) by A2, POLYNOM3:def 10
.= (Ext_eval (p1,a)) * (Ext_eval (q1,a)) by A5, ALGNUM_1:20
.= 0. E by A4 ;
then a is_a_root_of f,E ;
hence f is_with_roots_in E ; :: thesis: verum