theorem Th4: :: POLYALGX:4

for b being bag of 1 holds
( dom b = {0} & rng b = {(b . 0)} )