let R be domRing; :: thesis: for B being non zero bag of the carrier of R

for p being Ppoly of R,B

for a being Element of R st a in support B holds

eval (p,a) = 0. R

let F be non zero bag of the carrier of R; :: thesis: for p being Ppoly of R,F

for a being Element of R st a in support F holds

eval (p,a) = 0. R

let p be Ppoly of R,F; :: thesis: for a being Element of R st a in support F holds

eval (p,a) = 0. R

let a be Element of R; :: thesis: ( a in support F implies eval (p,a) = 0. R )

assume a in support F ; :: thesis: eval (p,a) = 0. R

then F . a <> 0 by PRE_POLY:def 7;

then (F . a) + 1 > 0 + 1 by XREAL_1:6;

then F . a >= 1 by NAT_1:13;

then multiplicity (p,a) >= 1 by dpp;

then consider s being Polynomial of R such that

A: p = (rpoly (1,a)) *' s by HURWITZ:33, UPROOTS:52;

thus eval (p,a) = 0. R by A, RING_4:1, Th9; :: thesis: verum

for p being Ppoly of R,B

for a being Element of R st a in support B holds

eval (p,a) = 0. R

let F be non zero bag of the carrier of R; :: thesis: for p being Ppoly of R,F

for a being Element of R st a in support F holds

eval (p,a) = 0. R

let p be Ppoly of R,F; :: thesis: for a being Element of R st a in support F holds

eval (p,a) = 0. R

let a be Element of R; :: thesis: ( a in support F implies eval (p,a) = 0. R )

assume a in support F ; :: thesis: eval (p,a) = 0. R

then F . a <> 0 by PRE_POLY:def 7;

then (F . a) + 1 > 0 + 1 by XREAL_1:6;

then F . a >= 1 by NAT_1:13;

then multiplicity (p,a) >= 1 by dpp;

then consider s being Polynomial of R such that

A: p = (rpoly (1,a)) *' s by HURWITZ:33, UPROOTS:52;

thus eval (p,a) = 0. R by A, RING_4:1, Th9; :: thesis: verum