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

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