:: deftheorem Def5 defines term POLYNOM7:def 5 :
for X being set
for L being non empty ZeroStr
for m being Monomial of X,L
for b₄ being bag of X holds
( b₄ = term m iff ( m . b₄ <> 0. L or ( Support m = {} & b₄ = EmptyBag X ) ) );