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)) +* ((EmptyBag X),a);

reconsider m = (0_ (X,L)) +* ((EmptyBag X),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)) +* ((EmptyBag X),b);

reconsider k = (0_ (X,L)) +* ((EmptyBag X),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 ((EmptyBag X) .--> a) by TARSKI:def 1;

A2: EmptyBag X in dom ((EmptyBag X) .--> b) by TARSKI:def 1;

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

.= Bags X ;

then A3: k . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> b)) . (EmptyBag X) by FUNCT_7:def 3

.= ((EmptyBag X) .--> b) . (EmptyBag X) by A2, FUNCT_4:13

.= b by FUNCOP_1:72 ;

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

.= Bags X ;

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

.= ((EmptyBag X) .--> a) . (EmptyBag X) by A1, FUNCT_4:13

.= a by FUNCOP_1:72 ;

hence ( a | (X,L) = b | (X,L) iff a = b ) by A3; :: thesis: verum

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)) +* ((EmptyBag X),a);

reconsider m = (0_ (X,L)) +* ((EmptyBag X),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)) +* ((EmptyBag X),b);

reconsider k = (0_ (X,L)) +* ((EmptyBag X),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 ((EmptyBag X) .--> a) by TARSKI:def 1;

A2: EmptyBag X in dom ((EmptyBag X) .--> b) by TARSKI:def 1;

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

.= Bags X ;

then A3: k . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> b)) . (EmptyBag X) by FUNCT_7:def 3

.= ((EmptyBag X) .--> b) . (EmptyBag X) by A2, FUNCT_4:13

.= b by FUNCOP_1:72 ;

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

.= Bags X ;

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

.= ((EmptyBag X) .--> a) . (EmptyBag X) by A1, FUNCT_4:13

.= a by FUNCOP_1:72 ;

hence ( a | (X,L) = b | (X,L) iff a = b ) by A3; :: thesis: verum