let m be multiset of I; :: thesis: m is finite-support
( 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 support m is finite by MONOID_1:def 6;
hence m is finite-support by PRE_POLY:def 8; :: thesis: verum