set Z = 0_ (X,L);
set O = (0_ (X,L)) +* ((EmptyBag X),a);
reconsider O = (0_ (X,L)) +* ((EmptyBag X),a) as Function of (Bags X), the carrier of L ;
reconsider O9 = O as Function of (Bags X),L ;
reconsider O9 = O9 as Series of X,L ;
now :: thesis: for b being bag of X st b <> EmptyBag X holds
O9 . b = 0. L
let b be bag of X; :: thesis: ( b <> EmptyBag X implies O9 . b = 0. L )
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
then A1: O9 = (0_ (X,L)) +* ((EmptyBag X) .--> a) by FUNCT_7:def 3;
assume b <> EmptyBag X ; :: thesis: O9 . b = 0. L
then not b in dom ((EmptyBag X) .--> a) by TARSKI:def 1;
hence O9 . b = (0_ (X,L)) . b by A1, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
:: thesis: verum
end;
hence a | (X,L) is Constant ; :: thesis: verum