Reducing a double ultrapower to a single ultrapower I hate having to ask this question, as I know for a fact I have seen the answer before but cannot seem to find it.  So I'm breaking down and asking for a reference.

Given a structure, let's say a Banach space $E$, and two ultrafilters $\mathfrak{U}$, and $\mathfrak{V}$ on $I$ and $J$ respectively.
We may of course form the Banach space Ultrapower $(E)_{\mathfrak{U}}$ which again gives a Banach space.  If we then take the ultrapower again, with respect to $\mathfrak{V}$, we get $[(E)_{\mathfrak{U}}]_{\mathfrak{V}}$.
I have seen (I am almost certain it was in the form of either an answer or a comment on this site) an argument that we can write $[(E)_{\mathfrak{U}}]_{\mathfrak{V}} = (E)_{\mathfrak{W}}$ for an appropriately defined ultrapower $\mathfrak{W}$ on $I\times J$.
I was wondering if anyone can provide a reference to the details of this?
 A: Suppose that $x=\langle x^{(j)}:j\in J\rangle\in (E^I)^J$, where each $x^{(j)}=\langle x_i^{(j)}:i\in I\rangle\in E^I$. Similarly, let $y=\langle y^{(j)}:j\in J\rangle\in (E^I)^J$, where each $y^{(j)}=\langle y_i^{(j)}:i\in I\rangle\in E^I$. Then we want to define $\mathfrak{W}$ so that 
$$\begin{align*}
x_{\mathfrak{W}}=y_{\mathfrak{W}}\quad&\text{iff}\quad\left\{j\in J:{x^{(j)}}_{\mathfrak{U}}={y^{(j)}}_{\mathfrak{U}}\right\}\in\mathfrak{V}\\
&\text{iff}\quad\left\{j\in J:\left\{i\in I:x_i^{(j)}=y_i^{(j)}\right\}\in\mathfrak{U}\right\}\in\mathfrak{V}\;.
\end{align*}$$
The ultrafilter product $\mathfrak{V}\cdot\mathfrak{U}$ is the ultrafilter on $J\times I$ such that for each $W\subseteq J\times I$,
$$W\in\mathfrak{V}\cdot\mathfrak{U}\quad\text{iff}\quad\big\{j\in J:\{i\in I:\langle j,i\rangle\in W\}\in\mathfrak{U}\big\}\in\mathfrak{V}\;.$$
From this it’s not hard to see that you want 
$$\mathfrak{W}=\{\langle i,j\rangle\in I\times J:\langle j,i\rangle\in\mathfrak{V}\cdot\mathfrak{U}\}\;.$$
The ultrafilter product that I’ve written $\mathfrak{V}\cdot\mathfrak{U}$ is denoted by $\otimes$ in this question; it is a special case of what is sometimes called the Fubini (or tensor) product of ultrafilters, and searching on that term will bring up assorted references; one that’s on the web, rather than a PDF or PostScript file, is here.
