let C be Category; :: thesis: for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i2 is initial holds
dom i1,c are_isomorphic

let c be Object of C; :: thesis: for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i2 is initial holds
dom i1,c are_isomorphic

let i1, i2 be Morphism of C; :: thesis: ( c is_a_coproduct_wrt i1,i2 & dom i2 is initial implies dom i1,c are_isomorphic )
set a = dom i1;
set b = dom i2;
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: dom i2 is initial ; :: thesis:
set f = id (dom i1);
set g = init ((dom i2),(dom i1));
( cod (init ((dom i2),(dom i1))) = dom i1 & dom (init ((dom i2),(dom i1))) = dom i2 ) by ;
then ( id (dom i1) in Hom ((dom i1),(dom i1)) & init ((dom i2),(dom i1)) in Hom ((dom i2),(dom i1)) ) by CAT_1:27;
then consider h being Morphism of C such that
A3: h in Hom (c,(dom i1)) and
A4: for k being Morphism of C st k in Hom (c,(dom i1)) holds
( ( k (*) i1 = id (dom i1) & k (*) i2 = init ((dom i2),(dom i1)) ) iff h = k ) by A1;
A5: cod h = dom i1 by ;
A6: cod i1 = c by A1;
then reconsider i = i1 as Morphism of dom i1,c by CAT_1:4;
A7: dom h = c by ;
then A8: dom (i (*) h) = c by ;
A9: cod i2 = c by A1;
then A10: dom ((i (*) h) (*) i2) = dom i2 by ;
A11: cod (i (*) h) = c by ;
then A12: i (*) h in Hom (c,c) by A8;
cod ((i (*) h) (*) i2) = c by ;
then A13: (i (*) h) (*) i2 = init ((dom i2),c) by
.= i2 by A2, A9, Th39 ;
A14: Hom ((dom i1),c) <> {} by ;
take i ; :: according to CAT_1:def 20 :: thesis: i is invertible
thus ( Hom ((dom i1),c) <> {} & Hom (c,(dom i1)) <> {} ) by ; :: according to CAT_1:def 16 :: thesis: ex b1 being Morphism of c, dom i1 st
( i * b1 = id c & b1 * i = id (dom i1) )

reconsider h = h as Morphism of c, dom i1 by ;
take h ; :: thesis: ( i * h = id c & h * i = id (dom i1) )
A15: (i (*) h) (*) i1 = i (*) (h (*) i1) by
.= i (*) (id (dom i)) by A3, A4
.= i by CAT_1:22 ;
thus i * h = i (*) h by
.= id c by A1, A13, A12, Th83, A15 ; :: thesis: h * i = id (dom i1)
thus id (dom i1) = h (*) i by A3, A4
.= h * i by ; :: thesis: verum