:: deftheorem defines is_a_coproduct_wrt CAT_3:def 18 :
for C being Category
for c being Object of C
for i1, i2 being Morphism of C holds
( c is_a_coproduct_wrt i1,i2 iff ( cod i1 = c & cod i2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) ) );