let C be Category; 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; 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; ( 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
; dom i1,c are_isomorphic
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 A2, Th42;
then
( id (dom i1) in Hom (dom i1),(dom i1) & init (dom i2),(dom i1) in Hom (dom i2),(dom i1) )
by CAT_1:55;
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, Def19;
A5:
cod h = dom i1
by A3, CAT_1:18;
A6:
cod i1 = c
by A1, Def19;
then reconsider i = i1 as Morphism of dom i1,c by CAT_1:22;
A7:
dom h = c
by A3, CAT_1:18;
then A8:
dom (i * h) = c
by A5, CAT_1:42;
A9:
cod i2 = c
by A1, Def19;
then A10:
dom ((i * h) * i2) = dom i2
by A8, CAT_1:42;
A11:
cod (i * h) = c
by A6, A5, CAT_1:42;
then A12:
i * h in Hom c,c
by A8;
cod ((i * h) * i2) = c
by A9, A11, A8, CAT_1:42;
then A13: (i * h) * i2 =
init (dom i2),c
by A2, A10, Th43
.=
i2
by A2, A9, Th43
;
thus
Hom (dom i1),c <> {}
by A6, CAT_1:19; CAT_1:def 17 ex b1 being Morphism of dom i1,c st b1 is invertible
take
i
; i is invertible
take
h
; CAT_1:def 12 ( 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:18; ( i * h = id (cod i) & h * i = id (dom i) )
(i * h) * i1 =
i * (h * i1)
by A6, A5, A7, CAT_1:43
.=
i * (id (dom i))
by A3, A4
.=
i
by CAT_1:47
;
hence
i * h = id (cod i)
by A1, A6, A13, A12, Th89; h * i = id (dom i)
thus
id (dom i) = h * i
by A3, A4; verum