theorem :: CAT_2:44

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