:: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def 6 :

for A being set

for b_{2} being non empty strict MonoidalSubStr of MultiSet_over A holds

( b_{2} = finite-MultiSet_over A iff for f being Multiset of A holds

( f in the carrier of b_{2} iff f " (NAT \ {0}) is finite ) );

for A being set

for b

( b

( f in the carrier of b