theorem :: CAT_2:45

for C, D being Category
for c being Object of C
for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d