:: deftheorem defines with_finite_product CAT_4:def 2 :
for C being Category holds
( C is with_finite_product iff for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) );