theorem Th60: :: CAT_4:61

for C being Cocartesian_category
for a, b being Object of C holds
( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b )