Let
\(M\subset \mathcal {S}_{\text {top}}\) be as in Lemma
2. The smooth coarea formula [
14, (A-2)] applied to the measurable function
\(f: M \rightarrow [0,+\infty )\) and to the submersion
\(p_1: M\rightarrow p_1(M)\) reads
$$\begin{aligned} \int \limits _{(a,x)\in M} NJ_{(a,x)} p_1\, f(a,x)\, \mathrm{d}(a,x) = \int \limits _{a\in p_1(M)} \sum \limits _{x\in S^1:\, (a,x)\in \mathcal {S}} f(a,x)\, \mathrm{d}a, \end{aligned}$$
(8)
where we used that
\(M=p_1^{-1}(p_1(M))\) (Lemma
2) to be able to sum over the whole fiber
\(p_1^{-1}(a)=\{(a,x)\in \mathcal {S}\},\, a\in p_1(M)\). By Lemma
2, we have
\(\text {dim}(\mathcal {S}{\setminus } M)\le m-1\), and hence,
\(\text {dim}(p_1(\mathcal {S}){\setminus } p_1(M))=\text {dim}(p_1(\mathcal {S}{\setminus } M))\le \text {dim}(\mathcal {S}{\setminus } M)\le m-1\). Thus, we extend the integrations in (
8) over
\(\mathcal {S}\) and
\(p_1(\mathcal {S})\), respectively, without changing the result. Moreover, the integration over
\(p_1(\mathcal {S})\) can be further extended to the whole space
\(\mathbb {R}^m\) since for a point
\(a\in \mathbb {R}^m{\setminus } p_1(\mathcal {S})\) the summation
\(\sum _{x\in S^1: (a,x)\in \mathcal {S}} f(a,x)\) is performed over the empty set
\(p_1^{-1}(a)\) and the sum is conventionally set to 0. All together, the above arguments imply
$$\begin{aligned} \int \limits _{(a,x)\in \mathcal {S}} NJ_{(a,x)} p_1\, f(a,x)\, \mathrm{d}(a,x) = \int \limits _{a\in \mathbb {R}^m} \sum \limits _{x\in S^1:\, (a,x)\in \mathcal {S}} f(a,x)\, \mathrm{d}a. \end{aligned}$$
(9)
Let
\(R\subset \mathcal {S}_{\text {top}}\) be as in Lemma
3. Applying the smooth coarea formula [
14, (A-2)] to the measurable function
\(\frac{NJ p_1}{NJ p_2} f: R \rightarrow [0,+\infty )\) and to the submersion
\(p_2: R\rightarrow p_2(R)\), we obtain
$$\begin{aligned} \int \limits _{(a,x)\in R} NJ_{(a,x)} p_1\, f(a,x)\, \mathrm{d}(a,x) = \int \limits _{x\in p_2(R)} \int \limits _{a\in p_2^{-1}(x)\cap R} \frac{NJ_{(a,x)} p_1}{NJ_{(a,x)} p_2} f(a,x)\, \mathrm{d}a\, \mathrm{d}x. \end{aligned}$$
(10)
By Lemma
3\(\text {dim}(\mathcal {S}{\setminus } R)\le m-1\),
\(S^1{\setminus } p_2(R)\) is finite, and
\(\text {dim}(p_2^{-1}(x){\setminus } R)\le m-2\) for
\(x\in p_2(R)\). Thus, the integrations in (
10) can be extended over
\(\mathcal {S}, S^1\) and
\(p_2^{-1}(x)\), respectively, leading to
$$\begin{aligned} \int \limits _{(a,x)\in \mathcal {S}} NJ_{(a,x)} p_1\, f(a,x)\, \mathrm{d}(a,x) = \int \limits _{x\in S^1} \int \limits _{a\in p_2^{-1}(x)} \frac{NJ_{(a,x)} p_1}{NJ_{(a,x)} p_2} f(a,x)\, \mathrm{d}a\, \mathrm{d}x. \end{aligned}$$
(11)
Combining (
11) with (
9), we finish the proof.
\(\square \)