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:22;

hence 0_ (X,L) is monomial-like ; :: thesis: verum

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:22;

hence 0_ (X,L) is monomial-like ; :: thesis: verum