set x = the Element of X;
set b = (EmptyBag X) +* ( the Element of X,1);
take (EmptyBag X) +* ( the Element of X,1) ; :: thesis: not (EmptyBag X) +* ( the Element of X,1) is empty
dom (EmptyBag X) = X by PARTFUN1:def 2;
then A1: ((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;
dom ( the Element of X .--> 1) = { the Element of X} by FUNCOP_1:13;
then the Element of X in dom ( the Element of X .--> 1) by TARSKI:def 1;
then ((EmptyBag X) +* ( the Element of X,1)) . the Element of X = ( the Element of X .--> 1) . the Element of X by A1, FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
then ((EmptyBag X) +* ( the Element of X,1)) . the Element of X <> (EmptyBag X) . the Element of X by PRE_POLY:52;
hence not (EmptyBag X) +* ( the Element of X,1) is empty by Def1; :: thesis: verum