theorem :: ALTCAT_6:5

for C being category
for A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
B is A -CatCoproduct-like