consider x being Element of X;
set b = (EmptyBag X) +* (x,1);
take (EmptyBag X) +* (x,1) ; :: thesis: (EmptyBag X) +* (x,1) is univariate
A1: dom (EmptyBag X) = X by PARTFUN1:def 4;
then A2: ((EmptyBag X) +* (x,1)) . x = ((EmptyBag X) +* (x .--> 1)) . x by FUNCT_7:def 3;
A3: dom (x .--> 1) = {x} by FUNCOP_1:19;
A4: for u being set st u in support ((EmptyBag X) +* (x,1)) holds
u in {x}

proof

let u be set ; :: thesis: ( u in support ((EmptyBag X) +* (x,1)) implies u in {x} )
assume A5: u in support ((EmptyBag X) +* (x,1)) ; :: thesis: u in {x}

now

assume u <> x ; :: thesis: contradiction
then A6: not u in dom (x .--> 1) by A3, TARSKI:def 1;
((EmptyBag X) +* (x,1)) . u = ((EmptyBag X) +* (x .--> 1)) . u by A1, FUNCT_7:def 3;
then ((EmptyBag X) +* (x,1)) . u = (EmptyBag X) . u by A6, FUNCT_4:12
.= 0 by PRE_POLY:52 ;
hence contradiction by A5, PRE_POLY:def 7; :: thesis: verum

end;

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

end;

x in dom (x .--> 1) by A3, TARSKI:def 1;
then A7: ((EmptyBag X) +* (x,1)) . x = (x .--> 1) . x by A2, FUNCT_4:14
.= 1 by FUNCOP_1:87 ;
for u being set st u in {x} holds
u in support ((EmptyBag X) +* (x,1))

proof

let u be set ; :: thesis: ( u in {x} implies u in support ((EmptyBag X) +* (x,1)) )
assume u in {x} ; :: thesis: u in support ((EmptyBag X) +* (x,1))
then u = x by TARSKI:def 1;
hence u in support ((EmptyBag X) +* (x,1)) by A7, PRE_POLY:def 7; :: thesis: verum

end;

then support ((EmptyBag X) +* (x,1)) = {x} by A4, TARSKI:2;
hence (EmptyBag X) +* (x,1) is univariate by Def3; :: thesis: verum