let F be 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
A: 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 A;
consider q being Element of the carrier of (Polynom-Ring F) such that
B: p * q = f by A, GCD_1:def 1;
consider E being FieldExtension of F such that
C: p is_with_roots_in E by kron;
take E ; :: thesis: f is_with_roots_in E
consider a being Element of E such that
D: a is_a_root_of p,E by C, FIELD_4:def 3;
reconsider p1 = p, q1 = q as Polynomial of F ;
F: F is Subring of E by FIELD_4:def 1;
Ext_eval (f,a) = Ext_eval ((p1 *' q1),a) by B, POLYNOM3:def 10
.= (Ext_eval (p1,a)) * (Ext_eval (q1,a)) by F, ALGNUM_1:20
.= (0. E) * (Ext_eval (q1,a)) by D, FIELD_4:def 2 ;
hence f is_with_roots_in E by FIELD_4:def 2, FIELD_4:def 3; :: thesis: verum