theorem Th29: :: BAGORDER:32

for n being Nat holds the carrier of (product (n --> OrderedNAT)) = Bags n