let L be non empty right_complementable Abelian add-associative right_zeroed distributive unital doubleLoopStr ; 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; for p being Polynomial of L st eval (p,z1) = z2 holds
eval ((p - <%z2%>),z1) = 0. L
let p be Polynomial of L; ( eval (p,z1) = z2 implies eval ((p - <%z2%>),z1) = 0. L )
assume A1:
eval (p,z1) = z2
; 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
; verum