theorem Th28: :: MONOID_1:28

for X being set
for m being Multiset of X holds
( dom m = X & rng m c= NAT )