:: deftheorem defines MultiSet_over MONOID_1:def 4 :
for A being set holds MultiSet_over A = .: (<NAT,+,0>,A);