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