let m1, m2 be Multiset of A; :: thesis: ( ( for a being Element of A holds m1 . a = card (dom ({a} |` p)) ) & ( for a being Element of A holds m2 . a = card (dom ({a} |` p)) ) implies m1 = m2 )
assume that
A2: for a being Element of A holds m1 . a = card (dom ({a} |` p)) and
A3: for a being Element of A holds m2 . a = card (dom ({a} |` p)) ; :: thesis: m1 = m2
now :: thesis: for a being Element of A holds m1 . a = m2 . a
let a be Element of A; :: thesis: m1 . a = m2 . a
thus m1 . a = card (dom ({a} |` p)) by A2
.= m2 . a by A3 ; :: thesis: verum
end;
hence m1 = m2 by Th32; :: thesis: verum