set x = the Element of X;
set b = (EmptyBag X) +* ( the Element of X,1);
take
(EmptyBag X) +* ( the Element of X,1)
; (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;
A4:
for u being object st u in support ((EmptyBag X) +* ( the Element of X,1)) holds
u in { the Element of X}
the Element of X in dom ( the Element of X .--> 1)
by 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 object st u in { the Element of X} holds
u in support ((EmptyBag X) +* ( the Element of X,1))
then
support ((EmptyBag X) +* ( the Element of X,1)) = { the Element of X}
by A4, TARSKI:2;
hence
(EmptyBag X) +* ( the Element of X,1) is univariate
; verum