:: deftheorem Def7 defines |. MONOID_1:def 7 :
for A being non empty set
for p being FinSequence of A
for b₃ being Multiset of A holds
( b₃ = |.p.| iff for a being Element of A holds b₃ . a = card (dom ({a} |` p)) );