:: deftheorem dpp1 defines Ppoly RING_5:def 4 :
for R being Ring
for b₂ being Polynomial of R holds
( b₂ is Ppoly of R iff ex F being non empty FinSequence of (Polynom-Ring R) st
( b₂ = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) ) );