let L be non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of L
for x being Element of L holds
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
let p be Polynomial of L; :: thesis: for x being Element of L holds
( eval (p,x) = 0. L iff rpoly (1,x) divides p )
let x be Element of L; :: thesis: ( eval (p,x) = 0. L iff rpoly (1,x) divides p )

A1: now :: thesis: ( rpoly (1,x) divides p implies eval (p,x) = 0. L )

assume rpoly (1,x) divides p ; :: thesis: eval (p,x) = 0. L
then p mod (rpoly (1,x)) = 0_. L ;
then (p - ((p div (rpoly (1,x))) *' (rpoly (1,x)))) + ((p div (rpoly (1,x))) *' (rpoly (1,x))) = (p div (rpoly (1,x))) *' (rpoly (1,x)) by POLYNOM3:28;
then A2: (p div (rpoly (1,x))) *' (rpoly (1,x)) = p + ((- ((p div (rpoly (1,x))) *' (rpoly (1,x)))) + ((p div (rpoly (1,x))) *' (rpoly (1,x)))) by POLYNOM3:26
.= p + (((p div (rpoly (1,x))) *' (rpoly (1,x))) - ((p div (rpoly (1,x))) *' (rpoly (1,x))))
.= p + (0_. L) by POLYNOM3:29
.= p by POLYNOM3:28 ;
A3: eval ((rpoly (1,x)),x) = x - x by HURWITZ:29
.= 0. L by RLVECT_1:15 ;
thus eval (p,x) = (eval ((p div (rpoly (1,x))),x)) * (0. L) by A3, A2, POLYNOM4:24
.= 0. L ; :: thesis: verum

end;

( eval (p,x) = 0. L implies rpoly (1,x) divides p ) by HURWITZ:35, POLYNOM5:def 7;
hence ( eval (p,x) = 0. L iff rpoly (1,x) divides p ) by A1; :: thesis: verum