theorem Th59: :: CAT_4:60

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