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 ;
A1: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
dom ((EmptyBag X) .--> a) = {(EmptyBag X)} by FUNCOP_1:19;
then A2: EmptyBag X in dom ((EmptyBag X) .--> a) by TARSKI:def 1;
A3: m . (EmptyBag X) = ((0_ X,L) +* ((EmptyBag X) .--> a)) . (EmptyBag X) by A1, FUNCT_7:def 3
.= ((EmptyBag X) .--> a) . (EmptyBag X) by A2, FUNCT_4:14
.= a by FUNCOP_1:87 ;
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 ;
A4: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
dom ((EmptyBag X) .--> b) = {(EmptyBag X)} by FUNCOP_1:19;
then A5: EmptyBag X in dom ((EmptyBag X) .--> b) by TARSKI:def 1;
k . (EmptyBag X) = ((0_ X,L) +* ((EmptyBag X) .--> b)) . (EmptyBag X) by A4, FUNCT_7:def 3
.= ((EmptyBag X) .--> b) . (EmptyBag X) by A5, FUNCT_4:14
.= b by FUNCOP_1:87 ;
hence ( a | X,L = b | X,L iff a = b ) by A3; :: thesis: verum