let X be set ; :: thesis: for L being non empty ZeroStr
for a, b being Element of L holds
( a | (X,L) = b | (X,L) iff a = b )

let L be non empty ZeroStr ; :: thesis: for a, b being Element of L holds
( a | (X,L) = b | (X,L) iff a = b )

let a, b be Element of L; :: thesis: ( a | (X,L) = b | (X,L) iff a = b )
set m = (0_ (X,L)) +* ((),a);
reconsider m = (0_ (X,L)) +* ((),a) 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 ;
set k = (0_ (X,L)) +* ((),b);
reconsider k = (0_ (X,L)) +* ((),b) as Function of (Bags X), the carrier of L ;
reconsider k = k as Function of (Bags X),L ;
reconsider k = k as Series of X,L ;
A1: EmptyBag X in dom (() .--> a) by TARSKI:def 1;
A2: EmptyBag X in dom (() .--> b) by TARSKI:def 1;
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
then A3: k . () = ((0_ (X,L)) +* (() .--> b)) . () by FUNCT_7:def 3
.= (() .--> b) . () by
.= b by FUNCOP_1:72 ;
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
then m . () = ((0_ (X,L)) +* (() .--> a)) . () by FUNCT_7:def 3
.= (() .--> a) . () by
.= a by FUNCOP_1:72 ;
hence ( a | (X,L) = b | (X,L) iff a = b ) by A3; :: thesis: verum