let Y, X be set ; :: thesis: chi Y,X is Multiset of X
A1: ( dom (chi Y,X) = X & rng (chi Y,X) c= {0 ,1} & H₃( MultiSet_over X) = Funcs X,NAT ) by Th27, FUNCT_3:def 3;
then rng (chi Y,X) c= NAT by XBOOLE_1:1;
hence chi Y,X is Multiset of X by A1, FUNCT_2:def 2; :: thesis: verum