let L be non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ; for p, q being Polynomial of L
for x being Element of L holds
( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )
let p, q be Polynomial of L; for x being Element of L holds
( not rpoly (1,x) divides p *' q or rpoly (1,x) divides p or rpoly (1,x) divides q )
let x be Element of L; ( 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
; ( 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;