theorem :: CAT_4:63

for C being Cocartesian_category
for a, b being Object of C holds a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) by Def26;