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