theorem Th12: :: POLYNOM9:12

for X being non empty set
for x being Element of X
for i being Element of NAT holds (EmptyBag X) +* (x,i) = ({x},i) -bag