theorem :: POLYNOM7:16

for X being set
for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( term c = EmptyBag X & coefficient c = c . (EmptyBag X) ) by Lm2;