Closure under products of split weights

For every universe-level-0 triple of types $X,A,B$, finite enumerations of $A$ and $B$, and split-weight data $D_1$ and $D_2$ on $X$ indexed by $A$ and $B$, form the datum indexed by $A×B$ whose coefficient at $(a,b)$ is $D_1.coefficient(a)D_2.coefficient(b)$ and whose feature at $((a,b),x)$ is $D_1.feature(a,x)D_2.feature(b,x)$. Then all three of the following hold: for every $l,r∈X$, the product datum's associated weight equals $D_1.weight(l,r)D_2.weight(l,r)$; if every coefficient of each original datum is nonnegative, then every coefficient of the product datum is nonnegative; and if each original datum's associated weight is nonnegative for every $l,r∈X$, then the product datum's associated weight is nonnegative for every $l,r∈X$. No finiteness assumption is made on $X$. If $A$ or $B$ is empty, the corresponding coefficient conditions and the conclusion over $A×B$ may be vacuous; if $X$ is empty, all assertions quantified over $l,r∈X$ are vacuous.