let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for a being Element of (Polynom-Ring p) holds a in the carrier of (Polynom-Ring F)
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of (Polynom-Ring p) holds a in the carrier of (Polynom-Ring F)
let a be Element of (Polynom-Ring p); :: thesis: a in the carrier of (Polynom-Ring F)
the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;
then a in { q where q is Polynomial of F : deg q < deg p } ;
then ex r being Polynomial of F st
( r = a & deg r < deg p ) ;
hence a in the carrier of (Polynom-Ring F) by POLYNOM3:def 10; :: thesis: verum