set p = 0_ X,L;
take 0_ X,L ; :: thesis: 0_ X,L is monomial-like
for b9 being bag of X st b9 <> EmptyBag X holds
(0_ X,L) . b9 = 0. L by POLYNOM1:81;
hence 0_ X,L is monomial-like by Def4; :: thesis: verum