for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT)