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

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