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:40, 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 Th17, Th22, MONOID_0:46; :: thesis: verum