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 ;

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

hence
a | (X,L) is Constant
; :: thesis: verumO9 . 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;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