:: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def 6 :
for A being set
for b₂ being non empty strict MonoidalSubStr of MultiSet_over A holds
( b₂ = finite-MultiSet_over A iff for f being Multiset of A holds
( f in the carrier of b₂ iff f " (NAT \ {0}) is finite ) );