:: deftheorem defines coefficient POLYNOM7:def 6 :
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L holds coefficient m = m . (term m);