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

let b be bag of X; :: thesis: ( b <> EmptyBag X implies O9 . b = 0. L )
A1: dom ((EmptyBag X) .--> a) = {(EmptyBag X)} by FUNCOP_1:13;
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 7
.= Bags X by FUNCOP_1:13 ;
then A2: 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 A1, TARSKI:def 1;
hence O9 . b = (0_ (X,L)) . b by A2, FUNCT_4:11
.= 0. L by POLYNOM1:22 ;
:: thesis: verum

end;

hence a | (X,L) is Constant by Def8; :: thesis: verum