theorem Th70: :: CAT_8:70

for C being non empty with_binary_products with_exponential_objects category
for a, b being Object of C holds
( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b )