補題
>>503の条件の下で g を X/H 上の実数値連続関数とする。
f(gp) は K(X, R) の元であるから (f(gp))^♭ が定義できる。

このとき、(f(gp))^♭ = (f^♭)g である。

証明
>>499より、(f(gp))^1 = (f^1)gp である。
即ち、((f(gp))^♭)p = (f^♭)p(gp)
よって、(f(gp))^♭ = (f^♭)g である。
証明終