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 (x .--> 1) = {x} by FUNCOP_1:19;
then A1: x in dom (x .--> 1) by TARSKI:def 1;
dom (EmptyBag X) = X by PARTFUN1:def 4;
then ((EmptyBag X) +* x,1) . x = ((EmptyBag X) +* (x .--> 1)) . x by FUNCT_7:def 3;
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 POLYNOM1:56;
hence not (EmptyBag X) +* x,1 is empty by Def1; :: thesis: verum