let R be domRing; :: thesis: for S being non empty finite Subset of R
for p being Ppoly of R,S
for a being Element of R st a in S holds
eval (p,a) = 0. R
let S be non empty finite Subset of R; :: thesis: for p being Ppoly of R,S
for a being Element of R st a in S holds
eval (p,a) = 0. R
let p be Ppoly of R,S; :: thesis: for a being Element of R st a in S holds
eval (p,a) = 0. R
let a be Element of R; :: thesis: ( a in S implies eval (p,a) = 0. R )
assume a in S ; :: thesis: eval (p,a) = 0. R
then consider q being Polynomial of R such that
H: (rpoly (1,a)) *' q = p by m0, RING_4:1;
a is_a_root_of p by H, prl2, HURWITZ:30;
hence eval (p,a) = 0. R by POLYNOM5:def 7; :: thesis: verum