let C be non empty with_binary_products category; :: thesis: for a, b, c1, c2 being Object of C
for e1 being Morphism of c1 [x] a,b
for e2 being Morphism of c2 [x] a,b st Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b holds
c1,c2 are_isomorphic
let a, b, c1, c2 be Object of C; :: thesis: for e1 being Morphism of c1 [x] a,b
for e2 being Morphism of c2 [x] a,b st Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b holds
c1,c2 are_isomorphic
let e1 be Morphism of c1 [x] a,b; :: thesis: for e2 being Morphism of c2 [x] a,b st Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b holds
c1,c2 are_isomorphic
let e2 be Morphism of c2 [x] a,b; :: thesis: ( Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b implies c1,c2 are_isomorphic )
assume A1: Hom ((c1 [x] a),b) <> {} ; :: thesis: ( not Hom ((c2 [x] a),b) <> {} or not c1,e1 is_exponent_of a,b or not c2,e2 is_exponent_of a,b or c1,c2 are_isomorphic )
assume A2: Hom ((c2 [x] a),b) <> {} ; :: thesis: ( not c1,e1 is_exponent_of a,b or not c2,e2 is_exponent_of a,b or c1,c2 are_isomorphic )
assume A3: c1,e1 is_exponent_of a,b ; :: thesis: ( not c2,e2 is_exponent_of a,b or c1,c2 are_isomorphic )
then A4: ( Hom (c2,c1) <> {} & ex h being Morphism of c2,c1 st
( e2 = e1 * (h [x] (id- a)) & ( for h1 being Morphism of c2,c1 st e2 = e1 * (h1 [x] (id- a)) holds
h = h1 ) ) ) by A2, A1, Def29;
assume A5: c2,e2 is_exponent_of a,b ; :: thesis: c1,c2 are_isomorphic
then A6: ( Hom (c1,c2) <> {} & ex h being Morphism of c1,c2 st
( e1 = e2 * (h [x] (id- a)) & ( for h1 being Morphism of c1,c2 st e1 = e2 * (h1 [x] (id- a)) holds
h = h1 ) ) ) by A1, A2, Def29;
ex f being Morphism of c1,c2 st f is isomorphism

proof

consider f being Morphism of c1,c2 such that
A7: ( e1 = e2 * (f [x] (id- a)) & ( for h1 being Morphism of c1,c2 st e1 = e2 * (h1 [x] (id- a)) holds
f = h1 ) ) by A1, A2, A5, Def29;
take f ; :: thesis: f is isomorphism
ex g being Morphism of c2,c1 st
( g * f = id- c1 & f * g = id- c2 )

proof

consider g being Morphism of c2,c1 such that
A8: ( e2 = e1 * (g [x] (id- a)) & ( for h1 being Morphism of c2,c1 st e2 = e1 * (h1 [x] (id- a)) holds
g = h1 ) ) by A2, A1, A3, Def29;
take g ; :: thesis: ( g * f = id- c1 & f * g = id- c2 )
A9: Hom (a,a) <> {} ;
A10: Hom ((c1 [x] a),(c2 [x] a)) <> {} by A9, A6, Th44;
A11: Hom ((c2 [x] a),(c1 [x] a)) <> {} by A9, A4, Th44;
consider h2 being Morphism of c1,c1 such that
e1 = e1 * (h2 [x] (id- a)) and
A12: for h1 being Morphism of c1,c1 st e1 = e1 * (h1 [x] (id- a)) holds
h2 = h1 by A3, A1, Def29;
e1 = e1 * ((g [x] (id- a)) * (f [x] (id- a))) by A7, A8, A10, A11, A1, CAT_7:23
.= e1 * ((g * f) [x] ((id- a) * (id- a))) by A4, A6, A9, Th66
.= e1 * ((g * f) [x] (id- a)) by A9, CAT_7:18 ;
then A13: g * f = h2 by A12;
e1 = e1 * (id- (c1 [x] a)) by A1, CAT_7:18
.= e1 * ((id- c1) [x] (id- a)) by Th67 ;
hence g * f = id- c1 by A12, A13; :: thesis: f * g = id- c2
consider h3 being Morphism of c2,c2 such that
e2 = e2 * (h3 [x] (id- a)) and
A14: for h1 being Morphism of c2,c2 st e2 = e2 * (h1 [x] (id- a)) holds
h3 = h1 by A5, A2, Def29;
e2 = e2 * ((f [x] (id- a)) * (g [x] (id- a))) by A7, A8, A10, A11, A2, CAT_7:23
.= e2 * ((f * g) [x] ((id- a) * (id- a))) by A4, A6, A9, Th66
.= e2 * ((f * g) [x] (id- a)) by A9, CAT_7:18 ;
then A15: f * g = h3 by A14;
e2 = e2 * (id- (c2 [x] a)) by A2, CAT_7:18
.= e2 * ((id- c2) [x] (id- a)) by Th67 ;
hence f * g = id- c2 by A14, A15; :: thesis: verum

end;

hence f is isomorphism by A4, A6, CAT_7:def 9; :: thesis: verum

end;

hence c1,c2 are_isomorphic by CAT_7:def 10; :: thesis: verum