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;
A4: for u being object st u in support ((EmptyBag X) +* ( the Element of X,1)) holds
u in { the Element of X}
proof
let u be object ; :: 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 :: thesis: not u <> the Element of X
assume u <> the Element of X ; :: thesis: contradiction
then A6: not u in dom ( the Element of X .--> 1) by 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 PBOOLE:5 ;
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 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))
proof
let u be object ; :: 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:2;
hence (EmptyBag X) +* ( the Element of X,1) is univariate ; :: thesis: verum