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 V3()
dom (EmptyBag X) = X ;
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;
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 ;
hence (EmptyBag X) +* ( the Element of X,1) is V3() ; :: thesis: verum