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}

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))

hence (EmptyBag X) +* ( the Element of X,1) is univariate ; :: thesis: verum

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

the Element of X in dom ( the Element of X .--> 1)
by TARSKI:def 1;
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}

end;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

hence
u in { the Element of X}
by TARSKI:def 1; :: thesis: verumassume
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;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

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

then
support ((EmptyBag X) +* ( the Element of X,1)) = { the Element of X}
by A4, TARSKI:2;
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;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

hence (EmptyBag X) +* ( the Element of X,1) is univariate ; :: thesis: verum