let C be non empty with_binary_products with_exponential_objects category; :: thesis: for a, b being Object of C holds
( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b )
let a, b be Object of C; :: thesis: ( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b )
set T = the categorical_exponent of a,b;
consider c being Object of C, e being Morphism of c [x] a,b such that
A1: ( the categorical_exponent of a,b = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b ) by Def31;
thus ( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b ) by A1; :: thesis: verum