let X,

Y be

set ;

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_{3}(

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;

verum