let x, X be set ; :: thesis: ( x is Multiset of X iff x is Function of X,NAT )

A1: now :: thesis: for x being Function of X,NAT holds x is Element of Funcs (X,NAT)

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;

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