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 i1 is initial holds
dom i2,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 i1 is initial holds
dom i2,c are_isomorphic
let i1, i2 be Morphism of C; :: thesis: ( c is_a_coproduct_wrt i1,i2 & dom i1 is initial implies dom i2,c are_isomorphic )
set a = dom i1;
set b = dom i2;
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: dom i1 is initial ; :: thesis: dom i2,c are_isomorphic
set f = id (dom i2);
set g = init ((dom i1),(dom i2));
( cod (init ((dom i1),(dom i2))) = dom i2 & dom (init ((dom i1),(dom i2))) = dom i1 ) by A2, Th42;
then ( id (dom i2) in Hom ((dom i2),(dom i2)) & init ((dom i1),(dom i2)) in Hom ((dom i1),(dom i2)) ) by CAT_1:26;
then consider h being Morphism of C such that
A3: h in Hom (c,(dom i2)) and
A4: for k being Morphism of C st k in Hom (c,(dom i2)) holds
( ( k * i1 = init ((dom i1),(dom i2)) & k * i2 = id (dom i2) ) iff h = k ) by A1, Def19;
A5: cod h = dom i2 by A3, CAT_1:1;
A6: cod i2 = c by A1, Def19;
then reconsider i = i2 as Morphism of dom i2,c by CAT_1:4;
A7: dom h = c by A3, CAT_1:1;
then A8: dom (i * h) = c by A5, CAT_1:17;
A9: cod i1 = c by A1, Def19;
then A10: dom ((i * h) * i1) = dom i1 by A8, CAT_1:17;
A11: cod (i * h) = c by A6, A5, CAT_1:17;
then A12: i * h in Hom (c,c) by A8;
cod ((i * h) * i1) = c by A9, A11, A8, CAT_1:17;
then A13: (i * h) * i1 = init ((dom i1),c) by A2, A10, Th43
.= i1 by A2, A9, Th43 ;
thus Hom ((dom i2),c) <> {} by A6, CAT_1:2; :: according to CAT_1:def 14 :: thesis: ex b₁ being Morphism of dom i2,c st b₁ is invertible
take i ; :: thesis: i is invertible
take h ; :: according to CAT_1:def 9 :: thesis: ( dom h = cod i & cod h = dom i & i * h = id (cod i) & h * i = id (dom i) )
thus ( dom h = cod i & cod h = dom i ) by A6, A3, CAT_1:1; :: thesis: ( i * h = id (cod i) & h * i = id (dom i) )
(i * h) * i2 = i * (h * i2) by A6, A5, A7, CAT_1:18
.= i * (id (dom i)) by A3, A4
.= i by CAT_1:22 ;
hence i * h = id (cod i) by A1, A6, A13, A12, Th89; :: thesis: h * i = id (dom i)
thus id (dom i) = h * i by A3, A4; :: thesis: verum