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