let X be set ; :: thesis: ( the carrier of (MultiSet_over X) = Funcs X,NAT & the multF of (MultiSet_over X) = addnat ,NAT .: X & 1. (MultiSet_over X) = X --> 0 )
( multMagma(# the carrier of <NAT,+,0> ,the multF of <NAT,+,0> #) = <NAT,+> & the_unity_wrt H₁( <NAT,+> ) = 0 ) by MONOID_0:44, MONOID_0:def 22;
hence ( the carrier of (MultiSet_over X) = Funcs X,NAT & the multF of (MultiSet_over X) = addnat ,NAT .: X & 1. (MultiSet_over X) = X --> 0 ) by Th18, Th23, MONOID_0:52; :: thesis: verum