let X be non empty set ; :: thesis:
let x be Element of X; :: thesis:

let a be object ; :: thesis:

hereby :: thesis:

assume A1: a in support (UnitBag x) ; :: thesis:

assume a <> x ; :: thesis:
then ((EmptyBag X) +* (x,1)) . a = (EmptyBag X) . a by FUNCT_7:32
.= 0 by PBOOLE:5 ;
hence contradiction by A1, PRE_POLY:def 7; :: thesis:

end;

hence a in {x} by TARSKI:def 1; :: thesis:

end;

EmptyBag X = X --> 0 by PBOOLE:def 3;
then A2: dom (EmptyBag X) = X ;
assume a in {x} ; :: thesis:
then a = x by TARSKI:def 1;
then (UnitBag x) . a = 1 by A2, FUNCT_7:31;
hence a in support (UnitBag x) by PRE_POLY:def 7; :: thesis:

end;

hence support (UnitBag x) = {x} by TARSKI:2; :: thesis: