let C be Category; :: thesis:
thus ( C is with_finite_product implies ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st
( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ) ) ) :: thesis:

proof

reconsider F = {} as Function of {}, the carrier of C by RELSET_1:12;
assume A1: for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) ; :: according to CAT_4:def 2 :: thesis:
then consider a being Object of C, F9 being Projections_family of a, {} such that
cods F9 = F and
A2: a is_a_product_wrt F9 ;
thus ex a being Object of C st a is terminal by A2, CAT_3:50; :: thesis:
let a, b be Object of C; :: thesis:
set F = (0,1) --> (a,b);
consider c being Object of C, F9 being Projections_family of c,{0,1} such that
A3: cods F9 = (0,1) --> (a,b) and
A4: c is_a_product_wrt F9 by A1;
take c ; :: thesis:
take p1 = F9 /. 0; :: thesis:
take p2 = F9 /. 1; :: thesis:
A5: 1 in {0,1} by TARSKI:def 2;
then A6: p2 = F9 . 1 by FUNCT_2:def 13;
A7: 0 in {0,1} by TARSKI:def 2;
hence ( dom p1 = c & dom p2 = c ) by A5, CAT_3:41; :: thesis:
( ((0,1) --> (a,b)) /. 0 = a & ((0,1) --> (a,b)) /. 1 = b ) by CAT_3:3;
hence ( cod p1 = a & cod p2 = b ) by A3, A7, A5, CAT_3:def 2; :: thesis:
( dom F9 = {0,1} & p1 = F9 . 0 ) by A7, FUNCT_2:def 1, FUNCT_2:def 13;
then F9 = (0,1) --> (p1,p2) by A6, FUNCT_4:66;
hence c is_a_product_wrt p1,p2 by A4, CAT_3:54; :: thesis:

end;

given a being Object of C such that A8: a is terminal ; :: 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 Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 );
assume A9: for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st
( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ; :: 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 Projections_family of a,I \ { the Element of I} such that
A13: cods G9 = G and
A14: a is_a_product_wrt G9 by A11;
consider c being Object of C, p1, p2 being Morphism of C such that
A15: dom p1 = c and
A16: dom p2 = c and
A17: cod p1 = a and
A18: cod p2 = F /. the Element of I and
A19: c is_a_product_wrt p1,p2 by A9;
set F9 = (G9 * p1) +* ( the Element of I .--> p2);
A20: dom ({ the Element of I} --> p2) = { the Element of I} by FUNCT_2:def 1;
rng ((G9 * p1) +* ( the Element of I .--> p2)) c= (rng (G9 * p1)) \/ (rng ( the Element of I .--> p2)) by FUNCT_4:17;
then A21: rng ((G9 * p1) +* ( the Element of I .--> p2)) c= the carrier' of C by XBOOLE_1:1;
dom (G9 * p1) = I \ { the Element of I} by FUNCT_2:def 1;
then A22: (dom (G9 * p1)) \/ (dom ( the Element of I .--> p2)) = I \/ { the Element of I} by A20, XBOOLE_1:39
.= I by A12, CARD_1:27, ZFMISC_1:40 ;
then dom ((G9 * p1) +* ( the Element of I .--> p2)) = I by FUNCT_4:def 1;
then reconsider F9 = (G9 * p1) +* ( the Element of I .--> p2) as Function of I, the carrier' of C by A21, FUNCT_2:def 1, RELSET_1:4;
A23: doms G9 = (I \ { the Element of I}) --> a by CAT_3:def 13;

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 .--> p2) . y by A20, A25, FUNCT_4:13
.= p2 by A25, FUNCOP_1:7 ;
hence (I --> c) . y = dom (F9 /. y) by A16, A24, FUNCOP_1:7
.= (doms F9) /. y by A24, CAT_3:def 1 ;
:: 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
.= (G9 * p1) . y by A20, A22, A24, A27, FUNCT_4:def 1
.= (G9 * p1) /. y by A28, FUNCT_2:def 13 ;
hence (doms F9) /. y = dom ((G9 * p1) /. y) by A24, CAT_3:def 1
.= (doms (G9 * p1)) /. y by A28, CAT_3:def 1
.= ((I \ { the Element of I}) --> c) /. y by A15, A17, A23, CAT_3:16
.= c by A24, A26, CAT_3:2, ZFMISC_1:56
.= (I --> c) . y by A24, FUNCOP_1:7 ;
:: thesis:

end;

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

end;

then reconsider F9 = F9 as Projections_family of c,I by CAT_3:def 13, 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 .--> p2) . y by A20, A32, FUNCT_4:13
.= p2 by A32, FUNCOP_1:7 ;
hence (cods F9) /. y = F /. y by A18, A30, A31, CAT_3:def 2; :: 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
.= (G9 * p1) . y by A20, A22, A30, A34, FUNCT_4:def 1
.= (G9 * p1) /. y by A35, FUNCT_2:def 13 ;
hence (cods F9) /. y = cod ((G9 * p1) /. y) by A30, CAT_3:def 2
.= (cods (G9 * p1)) /. y by A35, CAT_3:def 2
.= G /. y by A13, A17, A23, CAT_3:16
.= 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 (cods F9) /. y = F /. y ; :: thesis:

end;

hence cods F9 = F by CAT_3:1; :: thesis:
thus F9 is Projections_family of c,I ; :: according to CAT_3:def 14 :: thesis:
let d be Object of C; :: thesis:
let F99 be Projections_family of d,I; :: thesis:
assume A36: cods F9 = cods 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 (doms G99) /. y = dom (F99 /. y) by A37, CAT_3:def 1
.= d by A37, CAT_3:41
.= ((I \ { the Element of I}) --> d) /. y by A37, CAT_3:2 ;
:: thesis:

end;

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

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 (cods G9) /. y = cod (G99 /. y) by A13, A36, A38, A39, A29, CAT_3:1, CAT_3:def 2
.= (cods G99) /. y by A38, CAT_3:def 2 ;
:: thesis:

end;

then consider h9 being Morphism of C such that
A40: h9 in Hom (d,a) and
A41: for k being Morphism of C st k in Hom (d,a) holds
( ( for y being set st y in I \ { the Element of I} holds
(G9 /. y) (*) k = 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: dom (F99 /. the Element of I) = d by A12, CARD_1:27, CAT_3:41;
A44: F9 /. the Element of I = F9 . the Element of I by A12, CARD_1:27, FUNCT_2:def 13
.= ( the Element of I .--> p2) . the Element of I by A20, A42, FUNCT_4:13
.= p2 by A42, FUNCOP_1:7 ;
then cod p2 = (cods F9) /. the Element of I by A12, CARD_1:27, CAT_3:def 2
.= cod (F99 /. the Element of I) by A12, A36, CARD_1:27, CAT_3:def 2 ;
then F99 /. the Element of I in Hom (d,(cod p2)) by A43;
then consider h being Morphism of C such that
A45: h in Hom (d,c) and
A46: for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = h9 & p2 (*) k = F99 /. the Element of I ) iff h = k ) by A17, A19, A40;
take h ; :: thesis:
thus h in Hom (d,c) by A45; :: thesis:
let k be Morphism of C; :: thesis:
assume A47: k in Hom (d,c) ; :: thesis:
thus ( ( for y being set st y in I holds
(F9 /. y) (*) k = F99 /. y ) implies h = k ) :: thesis:

proof

A48: cod k = c by A47, CAT_1:1;
then A49: cod (p1 (*) k) = a by A15, A17, CAT_1:17;
assume A50: for y being set st y in I holds
(F9 /. y) (*) k = F99 /. y ; :: thesis:
A51: for y being set st y in I \ { the Element of I} holds
(G9 /. y) (*) (p1 (*) k) = 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
.= (G9 * p1) . y by A20, A22, A52, A53, FUNCT_4:def 1
.= (G9 * p1) /. y by A52, FUNCT_2:def 13 ;
dom (G9 /. y) = a by A52, CAT_3:41;
hence (G9 /. y) (*) (p1 (*) k) = ((G9 /. y) (*) p1) (*) k by A15, A17, A48, CAT_1:18
.= ((G9 * p1) /. y) (*) k by A52, CAT_3:def 5
.= 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;

dom k = d by A47, CAT_1:1;
then dom (p1 (*) k) = d by A15, A48, CAT_1:17;
then p1 (*) k in Hom (d,a) by A49;
then A55: p1 (*) k = h9 by A41, A51;
p2 (*) k = 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 .--> p2) . y by A20, A59, FUNCT_4:13
.= p2 by A59, FUNCOP_1:7 ;
hence (F9 /. y) (*) k = 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: cod k = c by A47, CAT_1:1;
A63: y in I \ { the Element of I} by A57, A60, ZFMISC_1:56;
A64: dom (G9 /. y) = a by A57, A60, CAT_3:41, ZFMISC_1:56;
F9 /. y = F9 . y by A57, FUNCT_2:def 13
.= (G9 * p1) . y by A20, A22, A57, A61, FUNCT_4:def 1
.= (G9 * p1) /. y by A63, FUNCT_2:def 13
.= (G9 /. y) (*) p1 by A63, CAT_3:def 5 ;
hence (F9 /. y) (*) k = (G9 /. y) (*) (p1 (*) k) by A15, A17, A62, A64, CAT_1:18
.= (G9 /. y) (*) h9 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 (F9 /. y) (*) k = F99 /. y ; :: thesis:

end;

let I be finite set ; :: according to CAT_4:def 2 :: 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 Projections_family of a,I by A67, CAT_3:42;
take a ; :: thesis:
take F9 ; :: thesis:
for x being set st x in I holds
(cods F9) /. x = F /. x ;
hence cods F9 = F by CAT_3:1; :: thesis:
thus a is_a_product_wrt F9 by A8, A67, CAT_3:50; :: 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 Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) by A65; :: thesis: