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