[step:Sum the cross terms and apply chart-independence on each overlap]Using the decomposition of Step 3 in the first sum,
\begin{align*}
\sum_{i \in I_K} \int_{U_{\alpha(i)}} \rho_i \, \omega = \sum_{i \in I_K} \int_{U_{\alpha(i)}} \sum_{j \in J_K} \rho_i \sigma_j \, \omega.
\end{align*}
Because each chart-local integral $\int_{U_{\alpha(i)}}$ is, by its definition, the [Lebesgue integral](/page/Lebesgue%20Integral) of a single smooth coefficient function pulled back through $\varphi_{\alpha(i)}$, and finite sums commute with pulling back and with Lebesgue integration, we may bring the finite sum over $J_K$ outside the chart-local integral:
\begin{align*}
\sum_{i \in I_K} \int_{U_{\alpha(i)}} \sum_{j \in J_K} \rho_i \sigma_j \, \omega = \sum_{i \in I_K} \sum_{j \in J_K} \int_{U_{\alpha(i)}} \rho_i \sigma_j \, \omega = \sum_{(i,j) \in I_K \times J_K} \int_{U_{\alpha(i)}} \rho_i \sigma_j \, \omega,
\end{align*}
where the second equality is the rearrangement of a finite double sum. By Step 3, each integrand $\rho_i \sigma_j \omega$ is supported in $U_{\alpha(i)} \cap V_{\beta(j)}$, so the claim from Step 2 applies to the two positively oriented charts $(U_{\alpha(i)}, \varphi_{\alpha(i)})$ and $(V_{\beta(j)}, \psi_{\beta(j)})$ and gives
\begin{align*}
\int_{U_{\alpha(i)}} \rho_i \sigma_j \, \omega = \int_{V_{\beta(j)}} \rho_i \sigma_j \, \omega \qquad \text{for every } (i,j) \in I_K \times J_K.
\end{align*}
Substituting and reversing the algebraic manipulation on the $\sigma_j$ side,
\begin{align*}
\sum_{(i,j) \in I_K \times J_K} \int_{V_{\beta(j)}} \rho_i \sigma_j \, \omega = \sum_{j \in J_K} \int_{V_{\beta(j)}} \sum_{i \in I_K} \rho_i \sigma_j \, \omega = \sum_{j \in J_K} \int_{V_{\beta(j)}} \sigma_j \, \omega.
\end{align*}
Chaining the equalities,
\begin{align*}
\sum_{i \in I} \int_{U_{\alpha(i)}} \rho_i \, \omega = \sum_{i \in I_K} \int_{U_{\alpha(i)}} \rho_i \, \omega = \sum_{j \in J_K} \int_{V_{\beta(j)}} \sigma_j \, \omega = \sum_{j \in J} \int_{V_{\beta(j)}} \sigma_j \, \omega,
\end{align*}
where the outer equalities use the finiteness reduction of Step 1.[/step]