consider x being Element of X;
set b = (EmptyBag X) +* x,1;
take (EmptyBag X) +* x,1 ; :: thesis: not (EmptyBag X) +* x,1 is empty
dom (EmptyBag X) = X by PARTFUN1:def 4;
then A1: ((EmptyBag X) +* x,1) . x = ((EmptyBag X) +* (x .--> 1)) . x by FUNCT_7:def 3;
dom (x .--> 1) = {x} by FUNCOP_1:19;
then x in dom (x .--> 1) by TARSKI:def 1;
then ((EmptyBag X) +* x,1) . x = (x .--> 1) . x by A1, FUNCT_4:14
.= 1 by FUNCOP_1:87 ;
then ((EmptyBag X) +* x,1) . x <> (EmptyBag X) . x by PRE_POLY:52;
hence not (EmptyBag X) +* x,1 is empty by Def1; :: thesis: verum