theorem Th11: :: POLYALGX:11

NBag1 * BagN1 = id (Bags 1)