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_{1}( <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

( multMagma(# the carrier of <NAT,+,0>, the multF of <NAT,+,0> #) = <NAT,+> & the_unity_wrt H

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