theorem :: CAT_2:25

for C, D being Category
for cd being Object of [:C,D:] ex c being Object of C ex d being Object of D st cd = [c,d] by DOMAIN_1:1;