theorem
Th26
:
:: MONOID_1:26
for
X
being
set
holds
( the
carrier
of
(
MultiSet_over
X
)
=
Funcs
(
X
,
NAT
) & the
multF
of
(
MultiSet_over
X
)
=
(
addnat
,
NAT
)
.:
X
&
1.
(
MultiSet_over
X
)
=
X
-->
0
)