let F be Field; :: thesis: for p being non zero Polynomial of F
for c being non zero Element of F
for a being Element of F holds multiplicity ((c * p),a) = multiplicity (p,a)
let p be non zero Polynomial of F; :: thesis: for c being non zero Element of F
for a being Element of F holds multiplicity ((c * p),a) = multiplicity (p,a)
let c be non zero Element of F; :: thesis: for a being Element of F holds multiplicity ((c * p),a) = multiplicity (p,a)
let a be Element of F; :: thesis: multiplicity ((c * p),a) = multiplicity (p,a)
set n = multiplicity (p,a);
( (X- a) `^ (multiplicity (p,a)) divides p & not (X- a) `^ ((multiplicity (p,a)) + 1) divides p ) by FIELD_14:67;
then ( (X- a) `^ (multiplicity (p,a)) divides c * p & not (X- a) `^ ((multiplicity (p,a)) + 1) divides c * p ) by RING_5:15;
hence multiplicity ((c * p),a) = multiplicity (p,a) by FIELD_14:67; :: thesis: verum