theorem Th25: :: CAT_2:31

for C, D being Category
for c being Object of C
for d being Object of D holds id [c,d] = [(id c),(id d)]