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