let m be multiset of I; :: thesis: ( m is I -defined & m is natural-valued )
( m in the carrier of (finite-MultiSet_over I) & the carrier of (finite-MultiSet_over I) c= the carrier of (MultiSet_over I) ) by MONOID_0:23;
hence ( m is I -defined & m is natural-valued ) by MONOID_1:27; :: thesis: verum