命題
H を局所コンパクト空間 X に右から固有に作用(>>473)する
局所コンパクト群とする。
p: X → X/H を標準射とする。

f ∈ K(X/G, R) (過去スレ007の708) に対して fp を対応させることにより、
K(X/G, R) から K^1(X, R) (>>492) への全単射が得られる。

証明
>>491 前半より f ∈ K(X/G, R) のとき、fp ∈ K^1(X, R) である。
p は全射だから f, h ∈ K(X/G, R) で fp = hp なら f = h である。
よって、本命題の対応 f → fp は単射である。

g ∈ K^1(X, R) のとき、任意の x ∈ X に対して f(xH) = g(x) と
定義することにより X/G 上の関数が得られるが >>491 の後半より
f ∈ K(X/G, R) である。
よって、本命題の対応 f → fp は全射である。
証明終