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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in (chi a) " (NAT \ {0}) or x in {a} )
assume A1: x in (chi a) " (NAT \ {0}) ; :: thesis: x in {a}
then x in dom (chi a) by FUNCT_1:def 7;
then reconsider y = x as Element of A by Th28;
(chi a) . x in NAT \ {0} by A1, FUNCT_1:def 7;
then not (chi a) . y in {0} by XBOOLE_0:def 5;
then (chi a) . y <> 0 by TARSKI:def 1;
then y = a by Th31;
hence x in {a} by TARSKI:def 1; :: thesis: verum

end;

hence chi a is Element of (finite-MultiSet_over A) by Def6; :: thesis: verum