theorem Th14: :: POLYALGX:14

for b being bag of 1 holds rng (NBag1 | (Segm ((b . 0) + 1))) = { x where x is bag of 1 : x . 0 <= b . 0 }