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