theorem :: CAT_8:71

for C being non empty with_binary_products with_exponential_objects category
for a, b, c being Object of C st Hom ((c [x] a),b) <> {} holds
ex L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) st
( ( for f being Morphism of c [x] a,b
for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective )