米田の補題

自然変換$\alpha :y(A)\Rightarrow X$の自然性より図式
$$\mathcal{C}(A,A)\mathcal{C}(A,f):=f\circ -{\alpha }_{A}X(A)XfAf\mathcal{C}(A,A^{\prime }){\alpha }_{A^{\prime }}X(A^{\prime })A^{\prime }$$
の可換性より示される。

• 自然変換$\alpha ,\beta :y(A)\Rightarrow X$に対して、$T_{A,X}(\alpha )=T_{A,X}(\beta )$ならば$f\in \mathcal{C}(A,A^{\prime })$に対して
  $${\alpha }_{A^{\prime }}(f)={\alpha }_{A^{\prime }}(f\circ \mathsf{id})=Xf(T_{A,X}(\alpha ))=Xf(T_{A,X}(\beta ))={\beta }_{A^{\prime }}(f\circ \mathsf{id})={\beta }_{A^{\prime }}(f)$$
  より$\alpha =\beta$となるため、$T_{A,X}$は単射となる。
• $x\in X(A)$と$f\in \mathcal{C}(A,A^{\prime })$に対して${\alpha }_{A^{\prime }}(f):=Xf(x)$として射の族$\alpha =({\alpha }_{A^{\prime }})$を定めると、$g:A^{\prime }\to B^{\prime }$に対して
  $$(Xg\circ {\alpha }_{A^{\prime }})(f)=Xg({\alpha }_{A^{\prime }}(f))=Xg(Xf(x))=(X(g\circ f))x={\alpha }_{A^{\prime }}(g\circ f)=({\alpha }_{A^{\prime }}\circ \mathcal{C}(A,g))(f)$$
  より$Xg\circ {\alpha }_{A^{\prime }}={\alpha }_{A^{\prime }}\circ \mathcal{C}(A,g)$なため、$\alpha$は自然変換$y(A)\Rightarrow X$かつ$T_{A,X}(\alpha )=x$となるため、$T_{A,X}$は全射となる。

$f\in \mathcal{C}(A,A^{\prime })$と自然変換$\alpha :y(A)\Rightarrow X$に対して
$$\begin{array}{rl}(Xf\circ T_{A,X})(\alpha )& =Xf(T_{A,X}(\alpha ))\\ & =Xf({\alpha }_A({\mathsf{id}}_A))\\ & ={\alpha }_{A^{\prime }}(f)\\ & ={\alpha }_{A^{\prime }}({\mathsf{id}}_{A^{\prime }}\circ f)\\ & ={\alpha }_{A^{\prime }}(\mathcal{C}(A^{\prime },f)({\mathsf{id}}_{A^{\prime }}))\\ & =({\alpha }_{A^{\prime }}\circ \mathcal{C}(A^{\prime },f))({\mathsf{id}}_{A^{\prime }})\\ & =({\alpha }_{A^{\prime }}\circ y(f{)}_{A^{\prime }})({\mathsf{id}}_{A^{\prime }})\\ & =(\alpha \circ y(f){)}_{A^{\prime }}({\mathsf{id}}_{A^{\prime }})\\ & =T_{A^{\prime },X}(\alpha \circ y(f))\\ & =T_{A^{\prime },X}(\hat{\mathcal{C}}(y(f),X)(\alpha ))\\ & =(T_{A^{\prime },X}\circ \hat{\mathcal{C}}(y(f),X))(\alpha )\end{array}$$
より、$Xf\circ T_{A,X}=T_{A^{\prime },X}\circ \hat{\mathcal{C}}(y(f),X)$なため、図式
$$\hat{\mathcal{C}}(y(A),X)\hat{\mathcal{C}}(y(f),X)=-\circ y(f)T_{A,X}X(A)XfAf\hat{\mathcal{C}}(y(A^{\prime }),X)T_{A^{\prime },X}X(A^{\prime })A^{\prime }$$
は可換となる。

自然変換$\sigma :X\Rightarrow X^{\prime },\alpha :y(A)\Rightarrow X$に対して
$$\begin{array}{rl}({\sigma }_A\circ T_{A,X})(\alpha )& ={\sigma }_A(T_{A,X}(\alpha ))\\ & ={\sigma }_A({\alpha }_A({\mathsf{id}}_A))\\ & =({\sigma }_A\circ {\alpha }_A)({\mathsf{id}}_A)\\ & =(\sigma \circ \alpha {)}_A({\mathsf{id}}_A)\\ & =T_{A^{\prime },X}(\sigma \circ \alpha )\\ & =T_{A^{\prime },X}(\hat{\mathcal{C}}(y(A),\sigma )(\alpha ))\\ & =(T_{A^{\prime },X}\circ \hat{\mathcal{C}}(y(A),\sigma ))(\alpha )\end{array}$$
より、${\sigma }_A\circ T_{A,X}=T_{A^{\prime },X}\circ \hat{\mathcal{C}}(y(A),\sigma )$なため、図式
$$\hat{\mathcal{C}}(y(A),X)\hat{\mathcal{C}}(y(A),\sigma )=\sigma \circ -T_{A,X}X(A){\sigma }_{A}X\sigma \hat{\mathcal{C}}(y(A),X^{\prime })T_{A,X^{\prime }}{X}^{\prime }(A)X^{\prime }$$
は可換となる。

補題2(全単射の存在性) で得られる全単射の族$T=(T_{A,X}{)}_{A\in \mathcal{C},X\in \hat{\mathcal{C}}}$について、 補題3(全単射の自然性1) と 補題4(全単射の自然性2) により、$A\in \mathcal{C}$と$X\in \hat{\mathcal{C}}$について自然な同型$\hat{\mathcal{C}}(y(A),X)\stackrel{T}{\to }X(A)$となる。