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