theorem :: CAT_3:76

for y being set
for C being Category
for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)