:: deftheorem Def7 defines with_coproducts ALTCAT_6:def 7 :
for C being category holds
( C is with_coproducts iff for I being set
for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms ) );