for I being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds
for f being Morphism of d,c st f = F /. x holds
f is coretraction