let m be multiset of I; :: thesis: m is total
( 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;
then m is Function of I,NAT by MONOID_1:27;
hence m is total ; :: thesis: verum