let p be Series of X,L; :: thesis: ( p is Constant implies p is monomial-like )
assume p is Constant ; :: thesis: p is monomial-like
then for b being bag of X st b <> EmptyBag X holds
p . b = 0. L by Def8;
hence p is monomial-like by Def4; :: thesis: verum