>>14の同型 φ：Hom(ρ_*(F), E) → Hom(F, ρ~(E)) を具体的に書いてみよう。
f ∈ Hom(ρ_*(F), E)、b ∈ B、x ∈ F のとき φ(f)(x)(b) = f(b※x) = f(bx) である。

特に φ(f)(x)(1) = f(x) である。
τ：ρ~(E) → E を>>15で定義した写像とする。
τ・φ(f)(x) = f(x)
よって、τ・φ(f) = f
u = φ(f) とおけば τu = φ^(-)(u)