let F be domRing; :: thesis: for p being non zero Polynomial of F
for b being non zero Element of F
for a being Element of F holds multiplicity (p,a) = multiplicity ((b * p),a)
let p be non zero Polynomial of F; :: thesis: for b being non zero Element of F
for a being Element of F holds multiplicity (p,a) = multiplicity ((b * p),a)
let b be non zero Element of F; :: thesis: for a being Element of F holds multiplicity (p,a) = multiplicity ((b * p),a)
let a be Element of F; :: thesis: multiplicity (p,a) = multiplicity ((b * p),a)
set r = rpoly (1,a);
set np = multiplicity (p,a);
( (rpoly (1,a)) `^ (multiplicity (p,a)) divides b * p & not (rpoly (1,a)) `^ ((multiplicity (p,a)) + 1) divides p ) by multip, divi1;
then ( (rpoly (1,a)) `^ (multiplicity (p,a)) divides b * p & not (rpoly (1,a)) `^ ((multiplicity (p,a)) + 1) divides b * p ) by divi1ad;
hence multiplicity (p,a) = multiplicity ((b * p),a) by multip; :: thesis: verum