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 O' = O as Function of (Bags X),L ;
reconsider O' = O' as Series of X,L ;

now

let b be bag of ; :: thesis: ( b <> EmptyBag X implies O' . b = 0. L )
assume A1: b <> EmptyBag X ; :: thesis: O' . b = 0. L
dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
then A2: O' = (0_ X,L) +* ((EmptyBag X) .--> a) by FUNCT_7:def 3;
dom ((EmptyBag X) .--> a) = {(EmptyBag X)} by FUNCOP_1:19;
then not b in dom ((EmptyBag X) .--> a) by A1, TARSKI:def 1;
hence O' . b = (0_ X,L) . b by A2, FUNCT_4:12
.= 0. L by POLYNOM1:81 ;
:: thesis: verum

end;

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