set x = the Element of X;
set b = () +* ( the Element of X,1);
take () +* ( the Element of X,1) ; :: thesis: () +* ( the Element of X,1) is univariate
A1: dom () = X by PARTFUN1:def 2;
then A2: ((EmptyBag X) +* ( the Element of X,1)) . the Element of X = (() +* ( the Element of X .--> 1)) . the Element of X by FUNCT_7:def 3;
A4: for u being object st u in support (() +* ( the Element of X,1)) holds
u in { the Element of X}
proof
let u be object ; :: thesis: ( u in support (() +* ( the Element of X,1)) implies u in { the Element of X} )
assume A5: u in support (() +* ( 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 = (() +* ( the Element of X .--> 1)) . u by ;
then (() +* ( the Element of X,1)) . u = () . u by
.= 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: (() +* ( the Element of X,1)) . the Element of X = ( the Element of X .--> 1) . the Element of X by
.= 1 by FUNCOP_1:72 ;
for u being object st u in { the Element of X} holds
u in support (() +* ( the Element of X,1))
proof
let u be object ; :: thesis: ( u in { the Element of X} implies u in support (() +* ( the Element of X,1)) )
assume u in { the Element of X} ; :: thesis: u in support (() +* ( the Element of X,1))
then u = the Element of X by TARSKI:def 1;
hence u in support (() +* ( the Element of X,1)) by ; :: thesis: verum
end;
then support (() +* ( the Element of X,1)) = { the Element of X} by ;
hence (EmptyBag X) +* ( the Element of X,1) is univariate ; :: thesis: verum