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