let C be non empty with_binary_products category; 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; 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; 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; ( 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) <> {}
; ( 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) <> {}
; ( 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
; ( 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
; 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
;
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
;
( 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;
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;
verum
end;
hence
f is
isomorphism
by A4, A6, CAT_7:def 9;
verum
end;
hence
c1,c2 are_isomorphic
by CAT_7:def 10; verum