let C be Category; :: thesis: for c being Object of C

for h, i1, i2 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 h, i1, i2 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 h, i1, i2 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 18 :: 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:27;

( (id c) (*) i1 = i1 & (id c) (*) i2 = i2 ) by A1, CAT_1:21;

hence id c = i by A4, A5

.= h by A3, A4 ;

:: thesis: verum

for h, i1, i2 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 h, i1, i2 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 h, i1, i2 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 18 :: 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:27;

( (id c) (*) i1 = i1 & (id c) (*) i2 = i2 ) by A1, CAT_1:21;

hence id c = i by A4, A5

.= h by A3, A4 ;

:: thesis: verum