C を圏とする。
U, X を C の対象とする。

>>639より、任意の f: U → X に対して
Hom(1_U, 1_X)(f) = (1_X)f(1_U) = f

よって、Hom(1_U, 1_X) = 1_Hom(U, X)