let I be set ; :: thesis: for C being Category
for a being Object of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds
dom (F /. x) is initial ) holds
a is initial
let C be Category; :: thesis: for a being Object of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds
dom (F /. x) is initial ) holds
a is initial
let a be Object of C; :: thesis: for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds
dom (F /. x) is initial ) holds
a is initial
let F be Injections_family of a,I; :: thesis: ( a is_a_coproduct_wrt F & ( for x being set st x in I holds
dom (F /. x) is initial ) implies a is initial )
assume that
A1: a is_a_coproduct_wrt F and
A2: for x being set st x in I holds
dom (F /. x) is initial ; :: thesis: a is initial

now :: thesis: ( ( I = {} implies a is initial ) & ( for b being Object of C holds
( Hom (a,b) <> {} & ex h being Morphism of a,b st
for g being Morphism of a,b holds h = g ) ) )

thus ( I = {} implies a is initial ) by A1, Th75; :: thesis: for b being Object of C holds
( Hom (a,b) <> {} & ex h being Morphism of a,b st
for g being Morphism of a,b holds h = g )
let b be Object of C; :: thesis: ( Hom (a,b) <> {} & ex h being Morphism of a,b st
for g being Morphism of a,b holds h = g )
deffunc H₁( set ) -> Morphism of dom (F /. $1),b = init ((dom (F /. $1)),b);
consider F9 being Function of I, the carrier' of C such that
A3: for x being set st x in I holds
F9 /. x = H₁(x) from CAT_3:sch 1();

now :: thesis: for x being set st x in I holds
(cods F9) /. x = (I --> b) /. x

let x be set ; :: thesis: ( x in I implies (cods F9) /. x = (I --> b) /. x )
assume A4: x in I ; :: thesis: (cods F9) /. x = (I --> b) /. x
then A5: dom (F /. x) is initial by A2;
thus (cods F9) /. x = cod (F9 /. x) by A4, Def2
.= cod (init ((dom (F /. x)),b)) by A3, A4
.= b by A5, Th38
.= (I --> b) /. x by A4, Th2 ; :: thesis: verum

end;

then reconsider F9 = F9 as Injections_family of b,I by Def16, Th1;

now :: thesis: for x being set st x in I holds
(doms F) /. x = (doms F9) /. x

let x be set ; :: thesis: ( x in I implies (doms F) /. x = (doms F9) /. x )
assume A6: x in I ; :: thesis: (doms F) /. x = (doms F9) /. x
then A7: dom (F /. x) is initial by A2;
thus (doms F) /. x = dom (F /. x) by A6, Def1
.= dom (init ((dom (F /. x)),b)) by A7, Th38
.= dom (F9 /. x) by A3, A6
.= (doms F9) /. x by A6, Def1 ; :: thesis: verum

end;

then consider h being Morphism of C such that
A8: h in Hom (a,b) and
A9: for k being Morphism of C st k in Hom (a,b) holds
( ( for x being set st x in I holds
k (*) (F /. x) = F9 /. x ) iff h = k ) by A1, Def17, Th1;
thus Hom (a,b) <> {} by A8; :: thesis: ex h being Morphism of a,b st
for g being Morphism of a,b holds h = g
reconsider h = h as Morphism of a,b by A8, CAT_1:def 5;
take h = h; :: thesis: for g being Morphism of a,b holds h = g
let g be Morphism of a,b; :: thesis: h = g

now :: thesis: ( g in Hom (a,b) & ( for x being set st x in I holds
F9 /. x = g (*) (F /. x) ) )

thus g in Hom (a,b) by A8, CAT_1:def 5; :: thesis: for x being set st x in I holds
F9 /. x = g (*) (F /. x)
let x be set ; :: thesis: ( x in I implies F9 /. x = g (*) (F /. x) )
set c = dom (F /. x);
A10: dom g = a by A8, CAT_1:5;
assume A11: x in I ; :: thesis: F9 /. x = g (*) (F /. x)
then dom (F /. x) is initial by A2;
then consider f being Morphism of dom (F /. x),b such that
A12: for f9 being Morphism of dom (F /. x),b holds f = f9 by CAT_1:def 19;
A13: cod (F /. x) = a by A11, Th62;
then A14: dom (g (*) (F /. x)) = dom (F /. x) by A10, CAT_1:17;
cod g = b by A8, CAT_1:5;
then cod (g (*) (F /. x)) = b by A10, A13, CAT_1:17;
then g (*) (F /. x) in Hom ((dom (F /. x)),b) by A14;
then A15: g (*) (F /. x) is Morphism of dom (F /. x),b by CAT_1:def 5;
F9 /. x = init ((dom (F /. x)),b) by A3, A11;
hence F9 /. x = f by A12
.= g (*) (F /. x) by A12, A15 ;
:: thesis: verum

end;

hence h = g by A9; :: thesis: verum

end;

hence a is initial by CAT_1:def 19; :: thesis: verum