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 the categorical_exponent of a,b `1 is Object of C by A1; :: thesis: verum