for C being Cocartesian_category
for a, b being Object of C holds [$(in1 (a,b)),(in2 (a,b))$] = id (a + b)