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;
A1: Bags X = dom ((0. L) | X,L) by FUNCT_2:def 1;
A2: Bags X = dom (0_ X,L) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in Bags X implies ((0. L) | X,L) . b₁ = (0_ X,L) . b₁ )
assume x in Bags X ; :: thesis: ((0. L) | X,L) . b₁ = (0_ X,L) . b₁
then reconsider x' = x as bag of by POLYNOM1:def 14;
set m = (0_ X,L) +* (EmptyBag X),(0. L);
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 ;
A3: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
then A4: m = (0_ X,L) +* ((EmptyBag X) .--> (0. L)) by FUNCT_7:def 3;
A5: dom ((EmptyBag X) .--> (0. L)) = {(EmptyBag X)} by FUNCOP_1:19;
then A6: EmptyBag X in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def 1;
A7: m . (EmptyBag X) = ((0_ X,L) +* ((EmptyBag X) .--> (0. L))) . (EmptyBag X) by A3, FUNCT_7:def 3
.= ((EmptyBag X) .--> (0. L)) . (EmptyBag X) by A6, FUNCT_4:14
.= 0. L by FUNCOP_1:87 ;

per cases ( x' = EmptyBag X or x' <> EmptyBag X ) ;

suppose x' = EmptyBag X ; :: thesis: ((0. L) | X,L) . b₁ = (0_ X,L) . b₁

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

end;

suppose x' <> EmptyBag X ; :: thesis: ((0. L) | X,L) . b₁ = (0_ X,L) . b₁

then not x' in dom ((EmptyBag X) .--> (0. L)) by A5, TARSKI:def 1;
hence ((0. L) | X,L) . x = (0_ X,L) . x by A4, FUNCT_4:12; :: thesis: verum

end;

end;

end;

hence (0. L) | X,L = 0_ X,L by A1, A2, FUNCT_1:9; :: thesis: verum