KERML_ — Interpretation function co-domain expressed incorrectly

[From Brian Larson] In 8.4.3.1.2 (Core Semantics Mathematical Preliminaries), the co-domain of the interpretation function (.^_T) is expressed as

which seems to say all sequences in S begin with the same element of the universe d ₁, is this intended?

Express interpretation function co-domain with cross products

The interpretation function is the power set of S, which is specified incorrectly, as described by the filer. Rather than complicate the current set builder notation, or attempt infinite cartesian products with index sets, use repeated cross products to express it. These are usually interpreted as specifying sequences of all the combinations of things of the specified types, as intended for S, even tho cross product is not associative and doesn't formally mean this.