for C being Category
for c being Object of C
for h, i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom (c,c) & h (*) i1 = i1 & h (*) i2 = i2 holds
h = id c