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] ; :: thesis: 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; :: thesis: verum