let C be Category; :: thesis:
thus ( C is with_finite_coproduct implies ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) ) :: thesis:

proof

reconsider F = {} as Function of {}, the carrier of C by RELSET_1:12;
A1: 0 in {0,1} by TARSKI:def 2;
assume A2: for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) ; :: according to CAT_4:def 20 :: thesis:
then consider a being Object of C, F9 being Injections_family of a, {} such that
doms F9 = F and
A3: a is_a_coproduct_wrt F9 ;
thus ex a being Object of C st a is initial by A3, CAT_3:75; :: thesis:
let a, b be Object of C; :: thesis:
set F = (0,1) --> (a,b);
consider c being Object of C, F9 being Injections_family of c,{0,1} such that
A4: doms F9 = (0,1) --> (a,b) and
A5: c is_a_coproduct_wrt F9 by A2;
take c ; :: thesis:
take i1 = F9 /. 0; :: thesis:
take i2 = F9 /. 1; :: thesis:
A6: 1 in {0,1} by TARSKI:def 2;
then A7: i2 = F9 . 1 by FUNCT_2:def 13;
( ((0,1) --> (a,b)) /. 0 = a & ((0,1) --> (a,b)) /. 1 = b ) by CAT_3:3;
hence ( dom i1 = a & dom i2 = b ) by A4, A1, A6, CAT_3:def 1; :: thesis:
thus ( cod i1 = c & cod i2 = c ) by A1, A6, CAT_3:62; :: thesis:
( dom F9 = {0,1} & i1 = F9 . 0 ) by A1, FUNCT_2:def 1, FUNCT_2:def 13;
then F9 = (0,1) --> (i1,i2) by A7, FUNCT_4:66;
hence c is_a_coproduct_wrt i1,i2 by A5, CAT_3:79; :: thesis:

end;

given a being Object of C such that A8: a is initial ; :: thesis:
defpred S₁[ Nat] means for I being finite set
for F being Function of I, the carrier of C st card I = $1 holds
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 );
assume A9: for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ; :: thesis:
A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A11: S₁[n] ; :: thesis:
let I be finite set ; :: thesis:
let F be Function of I, the carrier of C; :: thesis:
assume A12: card I = n + 1 ; :: thesis:
set x = the Element of I;
reconsider Ix = I \ { the Element of I} as finite set ;
reconsider sx = { the Element of I} as finite set ;
reconsider G = F | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier of C by FUNCT_2:32;
card Ix = (card I) - (card sx) by A12, CARD_1:27, CARD_2:44, ZFMISC_1:31
.= (card I) - 1 by CARD_1:30
.= n by A12, XCMPLX_1:26 ;
then consider a being Object of C, G9 being Injections_family of a,I \ { the Element of I} such that
A13: doms G9 = G and
A14: a is_a_coproduct_wrt G9 by A11;
set b = F /. the Element of I;
consider c being Object of C, i1, i2 being Morphism of C such that
A15: dom i1 = a and
A16: dom i2 = F /. the Element of I and
A17: cod i1 = c and
A18: cod i2 = c and
A19: c is_a_coproduct_wrt i1,i2 by A9;
set F9 = (i1 * G9) +* ( the Element of I .--> i2);
A20: dom ({ the Element of I} --> i2) = { the Element of I} by FUNCT_2:def 1;
rng ((i1 * G9) +* ( the Element of I .--> i2)) c= (rng (i1 * G9)) \/ (rng ( the Element of I .--> i2)) by FUNCT_4:17;
then A21: rng ((i1 * G9) +* ( the Element of I .--> i2)) c= the carrier' of C by XBOOLE_1:1;
dom (i1 * G9) = I \ { the Element of I} by FUNCT_2:def 1;
then A22: (dom (i1 * G9)) \/ (dom ( the Element of I .--> i2)) = I \/ { the Element of I} by A20, XBOOLE_1:39
.= I by A12, CARD_1:27, ZFMISC_1:40 ;
then dom ((i1 * G9) +* ( the Element of I .--> i2)) = I by FUNCT_4:def 1;
then reconsider F9 = (i1 * G9) +* ( the Element of I .--> i2) as Function of I, the carrier' of C by A21, FUNCT_2:def 1, RELSET_1:4;
A23: cods G9 = (I \ { the Element of I}) --> a by CAT_3:def 16;

now :: thesis:

let y be object ; :: thesis:
assume A24: y in I ; :: thesis:

now :: thesis:

per cases ;

suppose y = the Element of I ; :: thesis:

then A25: y in { the Element of I} by TARSKI:def 1;
F9 /. y = F9 . y by A24, FUNCT_2:def 13
.= ( the Element of I .--> i2) . y by A20, A25, FUNCT_4:13
.= i2 by A25, FUNCOP_1:7 ;
hence (I --> c) . y = cod (F9 /. y) by A18, A24, FUNCOP_1:7
.= (cods F9) /. y by A24, CAT_3:def 2 ;
:: thesis:

end;

suppose A26: y <> the Element of I ; :: thesis:

then A27: not y in { the Element of I} by TARSKI:def 1;
A28: y in I \ { the Element of I} by A24, A26, ZFMISC_1:56;
F9 /. y = F9 . y by A24, FUNCT_2:def 13
.= (i1 * G9) . y by A20, A22, A24, A27, FUNCT_4:def 1
.= (i1 * G9) /. y by A28, FUNCT_2:def 13 ;
hence (cods F9) /. y = cod ((i1 * G9) /. y) by A24, CAT_3:def 2
.= (cods (i1 * G9)) /. y by A28, CAT_3:def 2
.= ((I \ { the Element of I}) --> c) /. y by A15, A17, A23, CAT_3:17
.= c by A24, A26, CAT_3:2, ZFMISC_1:56
.= (I --> c) . y by A24, FUNCOP_1:7 ;
:: thesis:

end;

hence (cods F9) . y = (I --> c) . y by A24, FUNCT_2:def 13; :: thesis:

end;

then reconsider F9 = F9 as Injections_family of c,I by CAT_3:def 16, FUNCT_2:12;
take c ; :: thesis:
take F9 ; :: thesis:

A29: now :: thesis:

let y be set ; :: thesis:
assume A30: y in I ; :: thesis:

now :: thesis:

per cases ;

suppose A31: y = the Element of I ; :: thesis:

then A32: y in { the Element of I} by TARSKI:def 1;
F9 /. y = F9 . y by A30, FUNCT_2:def 13
.= ( the Element of I .--> i2) . y by A20, A32, FUNCT_4:13
.= i2 by A32, FUNCOP_1:7 ;
hence (doms F9) /. y = F /. y by A16, A30, A31, CAT_3:def 1; :: thesis:

end;

suppose A33: y <> the Element of I ; :: thesis:

then A34: not y in { the Element of I} by TARSKI:def 1;
A35: y in I \ { the Element of I} by A30, A33, ZFMISC_1:56;
F9 /. y = F9 . y by A30, FUNCT_2:def 13
.= (i1 * G9) . y by A20, A22, A30, A34, FUNCT_4:def 1
.= (i1 * G9) /. y by A35, FUNCT_2:def 13 ;
hence (doms F9) /. y = dom ((i1 * G9) /. y) by A30, CAT_3:def 1
.= (doms (i1 * G9)) /. y by A35, CAT_3:def 1
.= G /. y by A13, A15, A23, CAT_3:17
.= G . y by A35, FUNCT_2:def 13
.= F . y by A30, A33, FUNCT_1:49, ZFMISC_1:56
.= F /. y by A30, FUNCT_2:def 13 ;
:: thesis:

end;

hence (doms F9) /. y = F /. y ; :: thesis:

end;

hence doms F9 = F by CAT_3:1; :: thesis:
thus F9 is Injections_family of c,I ; :: according to CAT_3:def 17 :: thesis:
let d be Object of C; :: thesis:
let F99 be Injections_family of d,I; :: thesis:
assume A36: doms F9 = doms F99 ; :: thesis:
reconsider G99 = F99 | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier' of C by FUNCT_2:32;

now :: thesis:

let y be set ; :: thesis:
assume A37: y in I \ { the Element of I} ; :: thesis:
then G99 /. y = G99 . y by FUNCT_2:def 13
.= F99 . y by A37, FUNCT_1:49
.= F99 /. y by A37, FUNCT_2:def 13 ;
hence (cods G99) /. y = cod (F99 /. y) by A37, CAT_3:def 2
.= d by A37, CAT_3:62
.= ((I \ { the Element of I}) --> d) /. y by A37, CAT_3:2 ;
:: thesis:

end;

then reconsider G99 = G99 as Injections_family of d,I \ { the Element of I} by CAT_3:1, CAT_3:def 16;

now :: thesis:

let y be set ; :: thesis:
assume A38: y in I \ { the Element of I} ; :: thesis:
then A39: G /. y = G . y by FUNCT_2:def 13
.= F . y by A38, FUNCT_1:49
.= F /. y by A38, FUNCT_2:def 13 ;
F99 /. y = F99 . y by A38, FUNCT_2:def 13
.= G99 . y by A38, FUNCT_1:49
.= G99 /. y by A38, FUNCT_2:def 13 ;
hence (doms G9) /. y = dom (G99 /. y) by A13, A29, A36, A38, A39, CAT_3:1, CAT_3:def 1
.= (doms G99) /. y by A38, CAT_3:def 1 ;
:: thesis:

end;

then consider h9 being Morphism of C such that
A40: h9 in Hom (a,d) and
A41: for k being Morphism of C st k in Hom (a,d) holds
( ( for y being set st y in I \ { the Element of I} holds
k (*) (G9 /. y) = G99 /. y ) iff h9 = k ) by A14, CAT_3:1;
A42: the Element of I in { the Element of I} by TARSKI:def 1;
set g = F99 /. the Element of I;
A43: cod (F99 /. the Element of I) = d by A12, CARD_1:27, CAT_3:62;
A44: F9 /. the Element of I = F9 . the Element of I by A12, CARD_1:27, FUNCT_2:def 13
.= ( the Element of I .--> i2) . the Element of I by A20, A42, FUNCT_4:13
.= i2 by A42, FUNCOP_1:7 ;
then dom i2 = (doms F9) /. the Element of I by A12, CARD_1:27, CAT_3:def 1
.= dom (F99 /. the Element of I) by A12, A36, CARD_1:27, CAT_3:def 1 ;
then F99 /. the Element of I in Hom ((dom i2),d) by A43;
then consider h being Morphism of C such that
A45: h in Hom (c,d) and
A46: for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = h9 & k (*) i2 = F99 /. the Element of I ) iff h = k ) by A15, A19, A40;
take h ; :: thesis:
thus h in Hom (c,d) by A45; :: thesis:
let k be Morphism of C; :: thesis:
assume A47: k in Hom (c,d) ; :: thesis:
thus ( ( for y being set st y in I holds
k (*) (F9 /. y) = F99 /. y ) implies h = k ) :: thesis:

proof

A48: dom k = c by A47, CAT_1:1;
then A49: dom (k (*) i1) = a by A15, A17, CAT_1:17;
assume A50: for y being set st y in I holds
k (*) (F9 /. y) = F99 /. y ; :: thesis:
A51: for y being set st y in I \ { the Element of I} holds
(k (*) i1) (*) (G9 /. y) = G99 /. y

proof

let y be set ; :: thesis:
assume A52: y in I \ { the Element of I} ; :: thesis:
then A53: not y in { the Element of I} by XBOOLE_0:def 5;
A54: F9 /. y = F9 . y by A52, FUNCT_2:def 13
.= (i1 * G9) . y by A20, A22, A52, A53, FUNCT_4:def 1
.= (i1 * G9) /. y by A52, FUNCT_2:def 13 ;
cod (G9 /. y) = a by A52, CAT_3:62;
hence (k (*) i1) (*) (G9 /. y) = k (*) (i1 (*) (G9 /. y)) by A15, A17, A48, CAT_1:18
.= k (*) ((i1 * G9) /. y) by A52, CAT_3:def 6
.= F99 /. y by A50, A52, A54
.= F99 . y by A52, FUNCT_2:def 13
.= G99 . y by A52, FUNCT_1:49
.= G99 /. y by A52, FUNCT_2:def 13 ;
:: thesis:

end;

cod k = d by A47, CAT_1:1;
then cod (k (*) i1) = d by A17, A48, CAT_1:17;
then k (*) i1 in Hom (a,d) by A49;
then A55: k (*) i1 = h9 by A41, A51;
k (*) i2 = F99 /. the Element of I by A12, A44, A50, CARD_1:27;
hence h = k by A46, A47, A55; :: thesis:

end;

assume A56: h = k ; :: thesis:
let y be set ; :: thesis:
assume A57: y in I ; :: thesis:

now :: thesis:

per cases ;

suppose A58: y = the Element of I ; :: thesis:

then A59: y in { the Element of I} by TARSKI:def 1;
F9 /. y = F9 . y by A57, FUNCT_2:def 13
.= ( the Element of I .--> i2) . y by A20, A59, FUNCT_4:13
.= i2 by A59, FUNCOP_1:7 ;
hence k (*) (F9 /. y) = F99 /. y by A46, A47, A56, A58; :: thesis:

end;

suppose A60: y <> the Element of I ; :: thesis:

then A61: not y in { the Element of I} by TARSKI:def 1;
A62: dom k = c by A47, CAT_1:1;
A63: y in I \ { the Element of I} by A57, A60, ZFMISC_1:56;
A64: cod (G9 /. y) = a by A57, A60, CAT_3:62, ZFMISC_1:56;
F9 /. y = F9 . y by A57, FUNCT_2:def 13
.= (i1 * G9) . y by A20, A22, A57, A61, FUNCT_4:def 1
.= (i1 * G9) /. y by A63, FUNCT_2:def 13
.= i1 (*) (G9 /. y) by A63, CAT_3:def 6 ;
hence k (*) (F9 /. y) = (k (*) i1) (*) (G9 /. y) by A15, A17, A62, A64, CAT_1:18
.= h9 (*) (G9 /. y) by A46, A47, A56
.= G99 /. y by A40, A41, A63
.= G99 . y by A63, FUNCT_2:def 13
.= F99 . y by A57, A60, FUNCT_1:49, ZFMISC_1:56
.= F99 /. y by A57, FUNCT_2:def 13 ;
:: thesis:

end;

hence k (*) (F9 /. y) = F99 /. y ; :: thesis:

end;

let I be finite set ; :: according to CAT_4:def 20 :: thesis:
let F be Function of I, the carrier of C; :: thesis:
A65: card I = card I ;
A66: S₁[ 0 ]

proof

let I be finite set ; :: thesis:
let F be Function of I, the carrier of C; :: thesis:
assume card I = 0 ; :: thesis:
then A67: I = {} ;
{} is Function of {}, the carrier' of C by RELSET_1:12;
then reconsider F9 = {} as Injections_family of a,I by A67, CAT_3:63;
take a ; :: thesis:
take F9 ; :: thesis:
for x being set st x in I holds
(doms F9) /. x = F /. x ;
hence doms F9 = F by CAT_3:1; :: thesis:
thus a is_a_coproduct_wrt F9 by A8, A67, CAT_3:75; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A66, A10);
hence ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) by A65; :: thesis: