let A be non empty set ; :: thesis: for m1, m2 being Multiset of A st ( for a being Element of A holds m1 . a = m2 . a ) holds

m1 = m2

let m1, m2 be Multiset of A; :: thesis: ( ( for a being Element of A holds m1 . a = m2 . a ) implies m1 = m2 )

assume for a being Element of A holds m1 . a = m2 . a ; :: thesis: m1 = m2

then for x being object st x in A holds

m1 . x = m2 . x ;

hence m1 = m2 by Th20; :: thesis: verum

m1 = m2

let m1, m2 be Multiset of A; :: thesis: ( ( for a being Element of A holds m1 . a = m2 . a ) implies m1 = m2 )

assume for a being Element of A holds m1 . a = m2 . a ; :: thesis: m1 = m2

then for x being object st x in A holds

m1 . x = m2 . x ;

hence m1 = m2 by Th20; :: thesis: verum