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