let R be domRing; 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; 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; 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; ( (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; verum