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 holds
( (rpoly (1,a)) `^ (B . a) divides p & not (rpoly (1,a)) `^ ((B . a) + 1) divides p )
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 holds
( (rpoly (1,a)) `^ (F . a) divides p & not (rpoly (1,a)) `^ ((F . a) + 1) divides p )
let p be Ppoly of R,F; :: thesis: for a being Element of R holds
( (rpoly (1,a)) `^ (F . a) divides p & not (rpoly (1,a)) `^ ((F . a) + 1) divides p )
let a be Element of R; :: thesis: ( (rpoly (1,a)) `^ (F . a) divides p & not (rpoly (1,a)) `^ ((F . a) + 1) divides p )
multiplicity (p,a) = F . a by dpp;
hence ( (rpoly (1,a)) `^ (F . a) divides p & not (rpoly (1,a)) `^ ((F . a) + 1) divides p ) by multip; :: thesis: verum