:: deftheorem Def29 defines is_exponent_of CAT_8:def 29 :
for C being non empty with_binary_products category
for a, b, c being Object of C
for e being Morphism of c [x] a,b st Hom ((c [x] a),b) <> {} holds
( c,e is_exponent_of a,b iff for d being Object of C
for f being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds
( Hom (d,c) <> {} & ex h being Morphism of d,c st
( f = e * (h [x] (id- a)) & ( for h1 being Morphism of d,c st f = e * (h1 [x] (id- a)) holds
h = h1 ) ) ) );