補題
R を実数体とする。
n を整数 ≧ 1 とする。
U ⊂ R^n を空でない開集合とし、ψ: U → R^n をC^r級(r ≧ 1)の単射で、
すべての p ∈ U で det(J_ψ(p)) ≠ 0 とする。
任意の y ∈ ψ(U) に対して y ∈ V_y ⊂ ψ(U) となる開集合 V_y があり、

∫[V_y] g(z) dz = ∫[U_y] g(ψ(x)) |det(J_ψ(x))| dx

となるとする。
ここで、U_y = ψ^(-1)(V_y) であり、
g: V_y → R は Supp(g) がコンパクトな任意の連続関数である。

このとき、>>141が成り立つ。

証明
Supp(f) はコンパクトだから Supp(f) ⊂ V_y_1 ∪ . . . ∪ V_y_r となる
ψ(U) の点 y_1, . . ., y_r がある。
過去スレ010の102より、R^n から [0, 1] への連続関数 g_1, ..., g_r で
各i で Supp(g_i) ⊂ V_y_i
x ∈ Supp(f) のとき g_1(x) + ... + g_r(x) = 1 となるものが存在する。

f = Σfg_i であり、Supp(fg_i) ⊂ V_y_i である。

よって、
∫ f(y) dy = ∫f(x)g_i(x) dx = Σ ∫ f(x)g_i(x) dx
= Σ∫ f(ψ(x))g_i(ψ(x)) |det(J_ψ(x))| dx
= ∫ Σf(ψ(x))g_i(ψ(x)) |det(J_ψ(x))| dx
= ∫ f(ψ(x)) |det(J_ψ(x))| dx
証明終