let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 )

A: 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 by HURWITZ:def 7;
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 B: (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 ;
C: 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 C, B, POLYNOM4:24
.= 0. L by VECTSP_1:6 ; :: thesis: verum

end;

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