let C be Category; :: thesis: for c being Object of C
for i1, i2, h being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom c,c & h * i1 = i1 & h * i2 = i2 holds
h = id c
let c be Object of C; :: thesis: for i1, i2, h being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom c,c & h * i1 = i1 & h * i2 = i2 holds
h = id c
let i1, i2, h be Morphism of C; :: thesis: ( c is_a_coproduct_wrt i1,i2 & h in Hom c,c & h * i1 = i1 & h * i2 = i2 implies h = id c )
assume that
A1: ( cod i1 = c & cod i2 = c ) and
A2: for d being Object of C
for f, g being Morphism of C st f in Hom (dom i1),d & g in Hom (dom i2),d holds
ex h being Morphism of C st
( h in Hom c,d & ( for k being Morphism of C st k in Hom c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) and
A3: ( h in Hom c,c & h * i1 = i1 & h * i2 = i2 ) ; :: according to CAT_3:def 19 :: thesis: h = id c
( i1 in Hom (dom i1),c & i2 in Hom (dom i2),c ) by A1;
then consider i being Morphism of C such that
i in Hom c,c and
A4: for k being Morphism of C st k in Hom c,c holds
( ( k * i1 = i1 & k * i2 = i2 ) iff i = k ) by A2;
A5: id c in Hom c,c by CAT_1:55;
( (id c) * i1 = i1 & (id c) * i2 = i2 ) by A1, CAT_1:46;
hence id c = i by A4, A5
.= h by A3, A4 ;
:: thesis: verum