consider c being Object of C, e being Morphism of c [x] a,b such that
A1:
( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b )
by Def30;
take
[c,e]
; ex c being Object of C ex e being Morphism of c [x] a,b st
( [c,e] = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b )
thus
ex c being Object of C ex e being Morphism of c [x] a,b st
( [c,e] = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b )
by A1; verum