:: deftheorem Def30 defines with_exponential_objects CAT_8:def 30 :
for C being non empty with_binary_products category holds
( C is with_exponential_objects iff for a, b being Object of C ex c being Object of C ex e being Morphism of c [x] a,b st
( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b ) );