let X be set ; :: thesis: for m being Multiset of X holds
( dom m = X & rng m c= NAT )
let m be Multiset of X; :: thesis: ( dom m = X & rng m c= NAT )
m is Function of X,NAT by Th27;
hence ( dom m = X & rng m c= NAT ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum