H を局所コンパクト空間 X に右から固有に作用(>>473)する
局所コンパクト群とする。
X/H は>>487より局所コンパクトである。
p: X → X/H を標準射とする。
X から実数体 R への連続関数 g で、
ある f ∈ K(X/H, R) (過去スレ007の708) に対して g = fp と書けるものを
特徴付けよう。

まず、x ∈ X, ξ ∈ H に対して p(xξ) = p(x) だから、
g(xξ) = g(x) である。
次に、Supp(f) はコンパクトだから、
>>489より、p(K) = Supp(f) となる X のコンパクト部分集合 K がある。
p^(-1)(Supp(f)) = KH である。

B = {y ∈ X/H; f(y) ≠ 0} とおく。
p は全射だから>>490より、(p^(-1)(B))~ = p^(-1)(B~) である。
p^(-1)(B) = {x ∈ X; f(p(x)) ≠ 0} = {x ∈ X; g(x)) ≠ 0}
であるから (p^(-1)(B))~ = Supp(g) である。
B~ = Supp(f) であるから Supp(g) = p^(-1)(Supp(f)) である。
よって、Supp(g) = KH である。

逆に、X から実数体 R への連続関数 g で、以下の条件を満たすとする。
1) x ∈ X, ξ ∈ H に対して g(xξ) = g(x) となる。

2) X のコンパクト部分集合 K があり、Supp(g) = KH となる。

このとき、f(xH) = g(x) と定義することにより、X/H 上の実数値関数 f が
得られる。
g = fp であり、g は連続であるから、>>468より f は連続である。
上と同様に、Supp(g) = p^(-1)(Supp(f)) である。
よって、Supp(f) = p(K) である。p(K) はコンパクトだから
f ∈ K(X/H, R) である。