set c = 0_ (X,L);
take 0_ (X,L) ; :: thesis: 0_ (X,L) is Constant
for b being bag of X st b <> EmptyBag X holds
(0_ (X,L)) . b = 0. L by POLYNOM1:22;
hence 0_ (X,L) is Constant ; :: thesis: verum