for L being domRing
for x being Element of L
for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))