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

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

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

( x is Multiset of X iff x is Element of Funcs (X,NAT) )
by Th26;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;( 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

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