let C be category; :: thesis: for A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
B is A -CatCoproduct-like
let A be ObjectsFamily of {},C; :: thesis: for B being Object of C st B is initial holds
B is A -CatCoproduct-like
let B be Object of C; :: thesis: ( B is initial implies B is A -CatCoproduct-like )
assume B is initial ; :: thesis: B is A -CatCoproduct-like
then ex P being MorphismsFamily of A,B st
( P is empty & P is coprojection-morphisms ) by Th2;
hence B is A -CatCoproduct-like ; :: thesis: verum