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