:: deftheorem dpp defines Ppoly RING_5:def 5 :
for R being domRing
for B being non zero bag of the carrier of R
for b₃ being Ppoly of R holds
( b₃ is Ppoly of R,B iff ( deg b₃ = card B & ( for a being Element of R holds multiplicity (b₃,a) = B . a ) ) );