let C be non empty category; :: thesis: for c1, c2, a, b being Object of C
for p1 being Morphism of a,c1
for p2 being Morphism of a,c2
for q1 being Morphism of b,c1
for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds
a,b are_isomorphic
let c1, c2, a, b be Object of C; :: thesis: for p1 being Morphism of a,c1
for p2 being Morphism of a,c2
for q1 being Morphism of b,c1
for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds
a,b are_isomorphic
let p1 be Morphism of a,c1; :: thesis: for p2 being Morphism of a,c2
for q1 being Morphism of b,c1
for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds
a,b are_isomorphic
let p2 be Morphism of a,c2; :: thesis: for q1 being Morphism of b,c1
for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds
a,b are_isomorphic
let q1 be Morphism of b,c1; :: thesis: for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds
a,b are_isomorphic
let q2 be Morphism of b,c2; :: thesis: ( Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 implies a,b are_isomorphic )
assume A1: ( Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} ) ; :: thesis: ( not a,p1,p2 is_product_of c1,c2 or not b,q1,q2 is_product_of c1,c2 or a,b are_isomorphic )
assume A2: a,p1,p2 is_product_of c1,c2 ; :: thesis: ( not b,q1,q2 is_product_of c1,c2 or a,b are_isomorphic )
assume A3: b,q1,q2 is_product_of c1,c2 ; :: thesis: a,b are_isomorphic
ex ff being Morphism of a,b ex gg being Morphism of b,a st
( Hom (a,b) <> {} & Hom (b,a) <> {} & gg * ff = id- a & ff * gg = id- b )

proof

consider f being Morphism of a,b such that
A4: ( q1 * f = p1 & q2 * f = p2 & ( for h1 being Morphism of a,b st q1 * h1 = p1 & q2 * h1 = p2 holds
f = h1 ) ) by A1, A3, Def10;
consider g being Morphism of b,a such that
A5: ( p1 * g = q1 & p2 * g = q2 & ( for h1 being Morphism of b,a st p1 * h1 = q1 & p2 * h1 = q2 holds
g = h1 ) ) by A1, A2, Def10;
take f ; :: thesis: ex gg being Morphism of b,a st
( Hom (a,b) <> {} & Hom (b,a) <> {} & gg * f = id- a & f * gg = id- b )
take g ; :: thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & g * f = id- a & f * g = id- b )
thus A6: Hom (a,b) <> {} by A1, A3, Def10; :: thesis: ( Hom (b,a) <> {} & g * f = id- a & f * g = id- b )
thus A7: Hom (b,a) <> {} by A1, A2, Def10; :: thesis: ( g * f = id- a & f * g = id- b )
set g11 = q1 * f;
set g12 = q2 * f;
consider h1 being Morphism of a,a such that
A8: ( p1 * h1 = q1 * f & p2 * h1 = q2 * f & ( for h being Morphism of a,a st p1 * h = q1 * f & p2 * h = q2 * f holds
h1 = h ) ) by A1, A2, Def10;
A9: p1 * (g * f) = q1 * f by A1, A5, A7, A6, CAT_7:23;
A10: p2 * (g * f) = q2 * f by A1, A5, A7, A6, CAT_7:23;
A11: p1 * (id- a) = q1 * f by A1, A4, CAT_7:18;
A12: p2 * (id- a) = q2 * f by A1, A4, CAT_7:18;
thus g * f = h1 by A8, A9, A10
.= id- a by A8, A11, A12 ; :: thesis: f * g = id- b
set g21 = p1 * g;
set g22 = p2 * g;
consider h2 being Morphism of b,b such that
A13: ( q1 * h2 = p1 * g & q2 * h2 = p2 * g & ( for h being Morphism of b,b st q1 * h = p1 * g & q2 * h = p2 * g holds
h2 = h ) ) by A1, A3, Def10;
A14: q1 * (f * g) = p1 * g by A1, A4, A7, A6, CAT_7:23;
A15: q2 * (f * g) = p2 * g by A1, A4, A7, A6, CAT_7:23;
A16: q1 * (id- b) = p1 * g by A1, A5, CAT_7:18;
A17: q2 * (id- b) = p2 * g by A1, A5, CAT_7:18;
thus f * g = h2 by A13, A14, A15
.= id- b by A13, A16, A17 ; :: thesis: verum

end;

hence a,b are_isomorphic by CAT_7:def 11; :: thesis: verum