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