I have proved the following:
Let $I=\bigcup _{k\in K}J_k$ be a partition of a set $I$. Consider of famility $(A_i)_{i\in I}$ of objects in a category $\mathsf C$. When all the products involved exist, the following isomorphism holds: $$\coprod_{i\in I}A_i \cong \coprod _{k\in K} \left( \coprod _{j\in J_k}A_j \right) $$
Now I want to formally prove that $$\coprod _{i\in I,j\in J}A_{i,j}\cong \coprod _{i\in I} \left( \coprod _{j\in J}A_{i,j} \right) $$ But I don't see how. I think it should follow as a special case of what I proved but I can't figure out exactly how.
Set $I' = I × J$ and $K = I$. Then $I' = \bigcup_{k∈K} J_k$ is a partition of $I'$ where $J_k = \{k\}×J$. Then use what you’ve proved on $\coprod_{(i,j) ∈ I×J} A_{i,j} = \coprod_{i' ∈ I'} A_{i'}$.