let F be Field; :: thesis: for f being Element of the carrier of (Polynom-Ring F) st not f is constant holds
ex p being irreducible Element of the carrier of (Polynom-Ring F) st emb (f,p) is with_roots
let f be Element of the carrier of (Polynom-Ring F); :: thesis: ( not f is constant implies ex p being irreducible Element of the carrier of (Polynom-Ring F) st emb (f,p) is with_roots )
assume not f is constant ; :: thesis: ex p being irreducible Element of the carrier of (Polynom-Ring F) st emb (f,p) is with_roots
then consider p being Element of the carrier of (Polynom-Ring F) such that
A2: p is_a_irreducible_factor_of f by Th4;
reconsider p = p as irreducible Element of the carrier of (Polynom-Ring F) by A2;
take p ; :: thesis: emb (f,p) is with_roots
consider q being Element of the carrier of (Polynom-Ring F) such that
A3: p * q = f by A2, GCD_1:def 1;
A4: emb (f,p) = ((PolyHom (emb p)) . p) * ((PolyHom (emb p)) . q) by A3, GROUP_6:def 6
.= (emb (p,p)) *' (emb (q,p)) by POLYNOM3:def 10 ;
KrRoot p is_a_root_of emb (p,p) by Th43;
then emb (p,p) is with_roots by POLYNOM5:def 8;
hence emb (f,p) is with_roots by A4; :: thesis: verum