theorem Th10: :: POLYALGX:10

BagN1 * NBag1 = id NAT