theorem Th75: :: CAT_3:75

for C being Category
for a being Object of C
for F being Injections_family of a, {} holds
( a is_a_coproduct_wrt F iff a is initial )