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

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