命題
H を局所コンパクト空間 X に右から固有に作用(>>473)する
局所コンパクト群とする。
β を H 上の左Haar測度とする。
λ を X/H 上の正値Radon測度とする。
λ^# を>>553で定義した X 上の正値Radon測度とする。
f を X から [0, +∞] への関数で、λ^#可測かつ
λ^#に関してσ有限(過去スレ010の465)とする。

このとき、X/H 上の関数 xH → ∫^*[H] f(xξ) dβ(ξ) はλ可測であり、
∫^*[X] f(x) dλ^#(x) = ∫^*[X/H] dλ(xH)∫^*[H] f(xξ) dβ(ξ)

証明
>>680より、u → β_u は漠連続(>>681)でスカラー的にλ可積分(>>682)である。
>>783より、λ^# = ∫ β_u dλ(u) である。
よって、>>769より、関数 u → ∫^*[X] f(x) dβ_u(x) はλ可測かつ
λに関してσ有限であり、
∫^*[X] f(x) dλ^#(x) = ∫^*[X/H] dλ(u) ∫^*[H] f(x) dβ_u(x) となる。

一方、>>779より、u = xH のとき、
∫^*[X] f(y) dβ_u(y) = ∫^*[H] f(xξ) dβ(ξ)
よって、
∫^*[X] f(x) dλ^#(x) = ∫^*[X/H] dλ(xH)∫^*[H] f(xξ) dβ(ξ)
証明終