let X, Y 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 Th26, FUNCT_3:def 3;
hence chi (Y,X) is Multiset of X by A1, FUNCT_2:def 2; :: thesis: verum