命題
H を局所コンパクト空間 X に右から固有に作用(>>473)する
局所コンパクト群とする。
β を H 上の左Haar測度とする。
x ∈ X に対して、u = xH とおき、β_u を>>677で定義した
X 上の正値Radon測度とする。
f を X から [0, +∞] への任意の関数とする。

このとき、

∫^*[X] f(y) dβ_u(y) = ∫^*[H] f(xξ) dβ(ξ)

証明
過去スレ011の806より明らか。