:: deftheorem defPg defines Poly FIELD_11:def 6 :
for F being Field
for m being Ordinal
for p being Polynomial of F
for b₄ being Polynomial of (card (nonConstantPolys F)),F holds
( b₄ = Poly (m,p) iff ( b₄ . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
b₄ . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
b₄ . b = 0. F ) ) );