theorem Th15: :: RING_EMB:15

for b being bag of 0 holds
( dom b = {} & b = EmptyBag {} & rng b = 0 & EmptyBag {} = {} --> 0 & Bags {} = {(EmptyBag {})} )