let X be non empty set ; :: thesis: for x being Element of X
for i being Element of NAT holds (EmptyBag X) +* (x,i) = ({x},i) -bag
let x be Element of X; :: thesis: for i being Element of NAT holds (EmptyBag X) +* (x,i) = ({x},i) -bag
let i be Element of NAT ; :: thesis: (EmptyBag X) +* (x,i) = ({x},i) -bag
dom (EmptyBag X) = X by PARTFUN1:def 2;
hence (EmptyBag X) +* (x,i) = (EmptyBag X) +* (x .--> i) by FUNCT_7:def 3
.= (EmptyBag X) +* ({x} --> i) by FUNCOP_1:def 9
.= ({x},i) -bag by UPROOTS:def 2 ;
:: thesis: verum