let I be set ; :: thesis: 1. (finite-MultiSet_over I) = EmptyBag I
( 1. (MultiSet_over I) = I --> 0 & I --> 0 = EmptyBag I ) by MONOID_1:26;
hence 1. (finite-MultiSet_over I) = EmptyBag I by MONOID_0:def 24; :: thesis: verum