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, Th38;

then ( id (dom i2) in Hom ((dom i2),(dom i2)) & init ((dom i1),(dom i2)) in Hom ((dom i1),(dom i2)) ) by CAT_1:27;

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;

A5: cod h = dom i2 by A3, CAT_1:1;

A6: cod i2 = c by A1;

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;

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, Th39

.= i1 by A2, A9, Th39 ;

A14: Hom ((dom i2),c) <> {} by A6, CAT_1:2;

take i ; :: according to CAT_1:def 20 :: thesis: i is invertible

thus ( Hom ((dom i2),c) <> {} & Hom (c,(dom i2)) <> {} ) by A6, A3, CAT_1:2; :: according to CAT_1:def 16 :: thesis: ex b_{1} being Morphism of c, dom i2 st

( i * b_{1} = id c & b_{1} * i = id (dom i2) )

reconsider h = h as Morphism of c, dom i2 by A3, CAT_1:def 5;

take h ; :: thesis: ( i * h = id c & h * i = id (dom i2) )

A15: (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 ;

thus i * h = i (*) h by A3, A14, CAT_1:def 13

.= id c by A1, A13, A12, Th83, A15 ; :: thesis: h * i = id (dom i2)

thus id (dom i2) = h (*) i by A3, A4

.= h * i by A3, A14, CAT_1:def 13 ; :: thesis: verum

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, Th38;

then ( id (dom i2) in Hom ((dom i2),(dom i2)) & init ((dom i1),(dom i2)) in Hom ((dom i1),(dom i2)) ) by CAT_1:27;

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;

A5: cod h = dom i2 by A3, CAT_1:1;

A6: cod i2 = c by A1;

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;

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, Th39

.= i1 by A2, A9, Th39 ;

A14: Hom ((dom i2),c) <> {} by A6, CAT_1:2;

take i ; :: according to CAT_1:def 20 :: thesis: i is invertible

thus ( Hom ((dom i2),c) <> {} & Hom (c,(dom i2)) <> {} ) by A6, A3, CAT_1:2; :: according to CAT_1:def 16 :: thesis: ex b

( i * b

reconsider h = h as Morphism of c, dom i2 by A3, CAT_1:def 5;

take h ; :: thesis: ( i * h = id c & h * i = id (dom i2) )

A15: (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 ;

thus i * h = i (*) h by A3, A14, CAT_1:def 13

.= id c by A1, A13, A12, Th83, A15 ; :: thesis: h * i = id (dom i2)

thus id (dom i2) = h (*) i by A3, A4

.= h * i by A3, A14, CAT_1:def 13 ; :: thesis: verum