let F be Field; :: thesis: for p, q being non zero Polynomial of F
for a being Element of F holds multiplicity (p,a) <= multiplicity ((p *' q),a)
let p, q be non zero Polynomial of F; :: thesis: for a being Element of F holds multiplicity (p,a) <= multiplicity ((p *' q),a)
let a be Element of F; :: thesis: multiplicity (p,a) <= multiplicity ((p *' q),a)
multiplicity ((p *' q),a) = (multiplicity (p,a)) + (multiplicity (q,a)) by UPROOTS:55;
hence multiplicity (p,a) <= multiplicity ((p *' q),a) by NAT_1:11; :: thesis: verum