let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: 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; :: thesis: 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; :: 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 div1;
then A: (eval (p,x)) * (eval (q,x)) = 0. L by POLYNOM4:24;

per cases ( eval (p,x) = 0. L or eval (q,x) = 0. L ) by A, VECTSP_2:def 1;

suppose eval (p,x) = 0. L ; :: thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q )

hence ( rpoly (1,x) divides p or rpoly (1,x) divides q ) by div1; :: thesis: verum

end;

suppose eval (q,x) = 0. L ; :: thesis: ( rpoly (1,x) divides p or rpoly (1,x) divides q )

hence ( rpoly (1,x) divides p or rpoly (1,x) divides q ) by div1; :: thesis: verum

end;

end;