let A be non empty set ; :: thesis: for a being Element of A holds chi a is Element of (finite-MultiSet_over A)
let a be Element of A; :: thesis: chi a is Element of (finite-MultiSet_over A)
(chi a) " (NAT \ {0 }) c= {a}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (chi a) " (NAT \ {0 }) or x in {a} )
assume x in (chi a) " (NAT \ {0 }) ; :: thesis: x in {a}
then A1: ( x in dom (chi a) & (chi a) . x in NAT \ {0 } & dom (chi a) = A ) by Th29, FUNCT_1:def 13;
then reconsider y = x as Element of A ;
not (chi a) . y in {0 } by A1, XBOOLE_0:def 5;
then (chi a) . y <> 0 by TARSKI:def 1;
then y = a by Th32;
hence x in {a} by TARSKI:def 1; :: thesis: verum

end;

then (chi a) " (NAT \ {0 }) is finite ;
hence chi a is Element of (finite-MultiSet_over A) by Def6; :: thesis: verum