let X be set ; :: thesis: for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L)

let L be non empty ZeroStr ; :: thesis: (0. L) | (X,L) = 0_ (X,L)

set o1 = (0. L) | (X,L);

set o2 = 0_ (X,L);

let L be non empty ZeroStr ; :: thesis: (0. L) | (X,L) = 0_ (X,L)

set o1 = (0. L) | (X,L);

set o2 = 0_ (X,L);

now :: thesis: for x being object st x in Bags X holds

((0. L) | (X,L)) . x = (0_ (X,L)) . x

hence
(0. L) | (X,L) = 0_ (X,L)
; :: thesis: verum((0. L) | (X,L)) . x = (0_ (X,L)) . x

set m = (0_ (X,L)) +* ((EmptyBag X),(0. L));

let x be object ; :: thesis: ( x in Bags X implies ((0. L) | (X,L)) . b_{1} = (0_ (X,L)) . b_{1} )

reconsider m = (0_ (X,L)) +* ((EmptyBag X),(0. L)) as Function of (Bags X), the carrier of L ;

reconsider m = m as Function of (Bags X),L ;

reconsider m = m as Series of X,L ;

assume x in Bags X ; :: thesis: ((0. L) | (X,L)) . b_{1} = (0_ (X,L)) . b_{1}

then reconsider x9 = x as bag of X ;

A1: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8

.= Bags X ;

then A2: m = (0_ (X,L)) +* ((EmptyBag X) .--> (0. L)) by FUNCT_7:def 3;

A3: EmptyBag X in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def 1;

A4: m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (0. L))) . (EmptyBag X) by A1, FUNCT_7:def 3

.= ((EmptyBag X) .--> (0. L)) . (EmptyBag X) by A3, FUNCT_4:13

.= 0. L by FUNCOP_1:72 ;

end;let x be object ; :: thesis: ( x in Bags X implies ((0. L) | (X,L)) . b

reconsider m = (0_ (X,L)) +* ((EmptyBag X),(0. L)) as Function of (Bags X), the carrier of L ;

reconsider m = m as Function of (Bags X),L ;

reconsider m = m as Series of X,L ;

assume x in Bags X ; :: thesis: ((0. L) | (X,L)) . b

then reconsider x9 = x as bag of X ;

A1: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8

.= Bags X ;

then A2: m = (0_ (X,L)) +* ((EmptyBag X) .--> (0. L)) by FUNCT_7:def 3;

A3: EmptyBag X in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def 1;

A4: m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (0. L))) . (EmptyBag X) by A1, FUNCT_7:def 3

.= ((EmptyBag X) .--> (0. L)) . (EmptyBag X) by A3, FUNCT_4:13

.= 0. L by FUNCOP_1:72 ;