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

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

hence
m1 = m2
by Th32; :: thesis: verumlet 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;thus m1 . a = card (dom ({a} |` p)) by A2

.= m2 . a by A3 ; :: thesis: verum