theorem
Th27
:
:: MONOID_1:27
for
x
,
X
being
set
holds
(
x
is
Multiset
of
X
iff
x
is
Function
of
X
,
NAT
)