for n being Nat
for R being domRing
for p being non zero Polynomial of R
for a being Element of R holds
( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )