let L be domRing; :: thesis: for p, q being Polynomial of L

for a being Element of L holds

( not rpoly (1,a) divides p *' q or rpoly (1,a) divides p or rpoly (1,a) divides q )

let p, q be Polynomial of L; :: thesis: for a being Element of L holds

( not rpoly (1,a) divides p *' q or rpoly (1,a) divides p or rpoly (1,a) divides q )

let x be Element of L; :: thesis: ( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )

assume rpoly (1,x) divides p *' q ; :: thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q )

then eval ((p *' q),x) = 0. L by Th9;

then A1: (eval (p,x)) * (eval (q,x)) = 0. L by POLYNOM4:24;

for a being Element of L holds

( not rpoly (1,a) divides p *' q or rpoly (1,a) divides p or rpoly (1,a) divides q )

let p, q be Polynomial of L; :: thesis: for a being Element of L holds

( not rpoly (1,a) divides p *' q or rpoly (1,a) divides p or rpoly (1,a) divides q )

let x be Element of L; :: thesis: ( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )

assume rpoly (1,x) divides p *' q ; :: thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q )

then eval ((p *' q),x) = 0. L by Th9;

then A1: (eval (p,x)) * (eval (q,x)) = 0. L by POLYNOM4:24;