theorem Th27: :: MONOID_1:27

for x, X being set holds
( x is Multiset of X iff x is Function of X,NAT )