for F being Field
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