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 `2 is Morphism of (b |^ a) [x] a,b
by A1; verum