let X be non empty set ; :: thesis: for x being Element of X holds support (UnitBag x) = {x}
let x be Element of X; :: thesis: support (UnitBag x) = {x}

now :: thesis: for a being object holds
( ( a in support (UnitBag x) implies a in {x} ) & ( a in {x} implies a in support (UnitBag x) ) )

let a be object ; :: thesis: ( ( a in support (UnitBag x) implies a in {x} ) & ( a in {x} implies a in support (UnitBag x) ) )

hereby :: thesis: ( a in {x} implies a in support (UnitBag x) )

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

now :: thesis: not a <> x

assume a <> x ; :: thesis: contradiction
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: verum

end;

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

end;

EmptyBag X = X --> 0 by PBOOLE:def 3;
then A2: dom (EmptyBag X) = X ;
assume a in {x} ; :: thesis: a in support (UnitBag x)
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: verum

end;

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