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

let a be set ; :: 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

assume a <> x ; :: thesis: contradiction
then ((EmptyBag X) +* x,1) . a = (EmptyBag X) . a by FUNCT_7:34
.= 0 by POLYNOM1:56 ;
hence contradiction by A1, POLYNOM1:def 7; :: thesis: verum

end;

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

end;

assume a in {x} ; :: thesis: a in support (UnitBag x)
then A2: a = x by TARSKI:def 1;
EmptyBag X = X --> 0 by POLYNOM1:def 15;
then dom (EmptyBag X) = X by FUNCOP_1:19;
then (UnitBag x) . a = 1 by A2, FUNCT_7:33;
hence a in support (UnitBag x) by POLYNOM1:def 7; :: thesis: verum

end;

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