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

proof

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

now

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

end;

hence u in { the Element of X} by TARSKI:def 1; :: thesis: verum

end;

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

proof

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

end;

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