for C being non empty with_binary_products category
for a, b, c1, c2 being Object of C
for e1 being Morphism of c1 [x] a,b
for e2 being Morphism of c2 [x] a,b st Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b holds
c1,c2 are_isomorphic