let x, X be set ; :: thesis: ( x is Multiset of X iff x is Function of X,NAT )
A1: ( x is Multiset of X iff x is Element of Funcs X,NAT ) by Th27;

now

let x be Function of X,NAT ; :: thesis: x is Element of Funcs X,NAT
( dom x = X & rng x c= NAT ) by FUNCT_2:def 1;
hence x is Element of Funcs X,NAT by FUNCT_2:def 2; :: thesis: verum

end;

hence ( x is Multiset of X iff x is Function of X,NAT ) by A1; :: thesis: verum