let F be Field; 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); 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
; 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; verum