let X be set ; :: thesis: for x being object
for s1, s2, b being bag of X st Subst (b,x,s1) = Subst (b,x,s2) holds
s1 = s2
let x be object ; :: thesis: for s1, s2, b being bag of X st Subst (b,x,s1) = Subst (b,x,s2) holds
s1 = s2
let s1, s2, b be bag of X; :: thesis: ( Subst (b,x,s1) = Subst (b,x,s2) implies s1 = s2 )
assume A1: Subst (b,x,s1) = Subst (b,x,s2) ; :: thesis: s1 = s2
A2: ( dom s1 = X & X = dom s2 ) by PARTFUN1:def 2;
for y being object st y in dom s1 holds
s1 . y = s2 . y

proof

let y be object ; :: thesis: ( y in dom s1 implies s1 . y = s2 . y )
assume A3: y in dom s1 ; :: thesis: s1 . y = s2 . y
A4: ( dom (Subst (b,x,s1)) = X & X = dom (Subst (b,x,s2)) ) by PARTFUN1:def 2;
((b +* (x,0)) . y) + (s2 . y) = (Subst (b,x,s2)) . y by A3, A4, VALUED_1:def 1
.= ((b +* (x,0)) . y) + (s1 . y) by A1, A3, A4, VALUED_1:def 1 ;
hence s1 . y = s2 . y ; :: thesis: verum

end;

hence s1 = s2 by A2; :: thesis: verum