:: deftheorem Def8 defines with_products ALTCAT_5:def 8 :
for C being category holds
( C is with_products iff for I being set
for A being ObjectsFamily of I,C ex B being Object of C ex P being MorphismsFamily of B,A st
( P is feasible & P is projection-morphisms ) );