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}

let a be Element of A; :: thesis: chi a is Element of (finite-MultiSet_over A)

(chi a) " (NAT \ {0}) c= {a}

proof

hence
chi a is Element of (finite-MultiSet_over A)
by Def6; :: thesis: verum
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;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