let L be non empty right_complementable Abelian add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for z1, z2 being Element of L
for p being Polynomial of L st eval (p,z1) = z2 holds
eval ((p - <%z2%>),z1) = 0. L
let z1, z2 be Element of L; :: thesis: for p being Polynomial of L st eval (p,z1) = z2 holds
eval ((p - <%z2%>),z1) = 0. L
let p be Polynomial of L; :: thesis: ( eval (p,z1) = z2 implies eval ((p - <%z2%>),z1) = 0. L )
assume A1: eval (p,z1) = z2 ; :: thesis: eval ((p - <%z2%>),z1) = 0. L
thus eval ((p - <%z2%>),z1) = (eval (p,z1)) - (eval (<%z2%>,z1)) by POLYNOM4:21
.= z2 - z2 by A1, POLYNOM5:37
.= 0. L by RLVECT_1:15 ; :: thesis: verum