let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) st emb p is isomorphism holds
p is with_roots
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: ( emb p is isomorphism implies p is with_roots )
set h = emb p;
assume A1: emb p is isomorphism ; :: thesis: p is with_roots
then reconsider K = KroneckerField (F,p) as F -homomorphic F -isomorphic Ring by RING_3:def 4;
reconsider h = emb p as Isomorphism of F,K by A1;
A2: Roots ((PolyHom h) . p) = { (h . a) where a is Element of F : a in Roots p } by Th39;
KrRoot p is_a_root_of emb (p,p) by Th43;
then KrRoot p in Roots ((PolyHom h) . p) by POLYNOM5:def 10;
then ex a being Element of F st
( KrRoot p = h . a & a in Roots p ) by A2;
hence p is with_roots ; :: thesis: verum