let C be Category; :: thesis:
thus ( C is with_finite_product implies ( ex a being Object of st a is terminal & ( for a, b being Object of ex c being Object of ex p1, p2 being Morphism of 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:25;
assume A1: for I being finite set
for F being Function of I,the carrier of C ex a being Object of ex F' being Projections_family of a,I st
( cods F' = F & a is_a_product_wrt F' ) ; :: according to CAT_4:def 3 :: thesis:
then consider a being Object of , F' being Projections_family of a, {} such that
cods F' = F and
A2: a is_a_product_wrt F' ;
a is terminal by A2, CAT_3:55;
hence ex a being Object of st a is terminal ; :: thesis:
let a, b be Object of ; :: thesis:
set F = 0 ,1 --> a,b;
consider c being Object of , F' being Projections_family of c,{0 ,1} such that
A3: cods F' = 0 ,1 --> a,b and
A4: c is_a_product_wrt F' by A1;
take c ; :: thesis:
take p1 = F' /. 0 ; :: thesis:
take p2 = F' /. 1; :: thesis:
A5: 1 in {0 ,1} by TARSKI:def 2;
then A6: p2 = F' . 1 by FUNCT_2:def 14;
A7: 0 in {0 ,1} by TARSKI:def 2;
hence ( dom p1 = c & dom p2 = c ) by A5, CAT_3:45; :: thesis:
( (0 ,1 --> a,b) /. 0 = a & (0 ,1 --> a,b) /. 1 = b ) by CAT_3:7;
hence ( cod p1 = a & cod p2 = b ) by A3, A7, A5, CAT_3:def 4; :: thesis:
( dom F' = {0 ,1} & p1 = F' . 0 ) by A7, FUNCT_2:def 14, FUNCT_2:def 1;
then F' = 0 ,1 --> p1,p2 by A6, FUNCT_4:69;
hence c is_a_product_wrt p1,p2 by A4, CAT_3:59; :: thesis:

end;

given a being Object of 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 ex F' being Projections_family of a,I st
( cods F' = F & a is_a_product_wrt F' );
assume A9: for a, b being Object of ex c being Object of ex p1, p2 being Morphism of 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:
consider x being Element of I;
reconsider Ix = I \ {x} as finite set ;
reconsider sx = {x} as finite set ;
reconsider G = F | (I \ {x}) as Function of I \ {x},the carrier of C by FUNCT_2:38;
{x} c= I by A12, CARD_1:47, ZFMISC_1:37;
then card Ix = (card I) - (card sx) by CARD_2:63
.= (card I) - 1 by CARD_1:50
.= n by A12, XCMPLX_1:26 ;
then consider a being Object of , G' being Projections_family of a,I \ {x} such that
A13: cods G' = G and
A14: a is_a_product_wrt G' by A11;
consider c being Object of , p1, p2 being Morphism of such that
A15: dom p1 = c and
A16: dom p2 = c and
A17: cod p1 = a and
A18: cod p2 = F /. x and
A19: c is_a_product_wrt p1,p2 by A9;
set F' = (G' * p1) +* (x .--> p2);
A20: dom ({x} --> p2) = {x} by FUNCT_2:def 1;
rng ((G' * p1) +* (x .--> p2)) c= (rng (G' * p1)) \/ (rng (x .--> p2)) by FUNCT_4:18;
then A21: rng ((G' * p1) +* (x .--> p2)) c= the carrier' of C by XBOOLE_1:1;
dom (G' * p1) = I \ {x} by FUNCT_2:def 1;
then A22: (dom (G' * p1)) \/ (dom (x .--> p2)) = I \/ {x} by A20, XBOOLE_1:39
.= I by A12, CARD_1:47, ZFMISC_1:46 ;
then dom ((G' * p1) +* (x .--> p2)) = I by FUNCT_4:def 1;
then reconsider F' = (G' * p1) +* (x .--> p2) as Function of I,the carrier' of C by A21, FUNCT_2:def 1, RELSET_1:11;
A23: doms G' = (I \ {x}) --> a by CAT_3:def 14;

now

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

now

per cases ;

suppose y = x ; :: thesis:

then A25: y in {x} by TARSKI:def 1;
F' /. y = F' . y by A24, FUNCT_2:def 14
.= (x .--> p2) . y by A20, A25, FUNCT_4:14
.= p2 by A25, FUNCOP_1:13 ;
hence (I --> c) . y = dom (F' /. y) by A16, A24, FUNCOP_1:13
.= (doms F') /. y by A24, CAT_3:def 3 ;
:: thesis:

end;

suppose A26: y <> x ; :: thesis:

then A27: not y in {x} by TARSKI:def 1;
A28: y in I \ {x} by A24, A26, ZFMISC_1:64;
F' /. y = F' . y by A24, FUNCT_2:def 14
.= (G' * p1) . y by A20, A22, A24, A27, FUNCT_4:def 1
.= (G' * p1) /. y by A28, FUNCT_2:def 14 ;
hence (doms F') /. y = dom ((G' * p1) /. y) by A24, CAT_3:def 3
.= (doms (G' * p1)) /. y by A28, CAT_3:def 3
.= ((I \ {x}) --> c) /. y by A15, A17, A23, CAT_3:20
.= c by A28, CAT_3:2
.= (I --> c) . y by A24, FUNCOP_1:13 ;
:: thesis:

end;

hence (doms F') . y = (I --> c) . y by A24, FUNCT_2:def 14; :: thesis:

end;

then doms F' = I --> c by FUNCT_2:18;
then reconsider F' = F' as Projections_family of c,I by CAT_3:def 14;
take c ; :: thesis:
take F' ; :: thesis:

now

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

now

per cases ;

suppose A30: y = x ; :: thesis:

then A31: y in {x} by TARSKI:def 1;
F' /. y = F' . y by A29, FUNCT_2:def 14
.= (x .--> p2) . y by A20, A31, FUNCT_4:14
.= p2 by A31, FUNCOP_1:13 ;
hence (cods F') /. y = F /. y by A18, A29, A30, CAT_3:def 4; :: thesis:

end;

suppose A32: y <> x ; :: thesis:

then A33: not y in {x} by TARSKI:def 1;
A34: y in I \ {x} by A29, A32, ZFMISC_1:64;
F' /. y = F' . y by A29, FUNCT_2:def 14
.= (G' * p1) . y by A20, A22, A29, A33, FUNCT_4:def 1
.= (G' * p1) /. y by A34, FUNCT_2:def 14 ;
hence (cods F') /. y = cod ((G' * p1) /. y) by A29, CAT_3:def 4
.= (cods (G' * p1)) /. y by A34, CAT_3:def 4
.= G /. y by A13, A17, A23, CAT_3:20
.= G . y by A34, FUNCT_2:def 14
.= F . y by A34, FUNCT_1:72
.= F /. y by A29, FUNCT_2:def 14 ;
:: thesis:

end;

hence (cods F') /. y = F /. y ; :: thesis:

end;

hence A35: cods F' = F by CAT_3:1; :: thesis:
thus F' is Projections_family of c,I ; :: according to CAT_3:def 15 :: thesis:
let d be Object of ; :: thesis:
let F'' be Projections_family of d,I; :: thesis:
assume A36: cods F' = cods F'' ; :: thesis:
reconsider G'' = F'' | (I \ {x}) as Function of I \ {x},the carrier' of C by FUNCT_2:38;

now

let y be set ; :: thesis:
assume A37: y in I \ {x} ; :: thesis:
then G'' /. y = G'' . y by FUNCT_2:def 14
.= F'' . y by A37, FUNCT_1:72
.= F'' /. y by A37, FUNCT_2:def 14 ;
hence (doms G'') /. y = dom (F'' /. y) by A37, CAT_3:def 3
.= d by A37, CAT_3:45
.= ((I \ {x}) --> d) /. y by A37, CAT_3:2 ;
:: thesis:

end;

then doms G'' = (I \ {x}) --> d by CAT_3:1;
then reconsider G'' = G'' as Projections_family of d,I \ {x} by CAT_3:def 14;

now

let y be set ; :: thesis:
assume A38: y in I \ {x} ; :: thesis:
then A39: G /. y = G . y by FUNCT_2:def 14
.= F . y by A38, FUNCT_1:72
.= F /. y by A38, FUNCT_2:def 14 ;
F'' /. y = F'' . y by A38, FUNCT_2:def 14
.= G'' . y by A38, FUNCT_1:72
.= G'' /. y by A38, FUNCT_2:def 14 ;
hence (cods G') /. y = cod (G'' /. y) by A13, A35, A36, A38, A39, CAT_3:def 4
.= (cods G'') /. y by A38, CAT_3:def 4 ;
:: thesis:

end;

then cods G' = cods G'' by CAT_3:1;
then consider h' being Morphism of such that
A40: h' in Hom d,a and
A41: for k being Morphism of st k in Hom d,a holds
( ( for y being set st y in I \ {x} holds
(G' /. y) * k = G'' /. y ) iff h' = k ) by A14, CAT_3:def 15;
A42: x in {x} by TARSKI:def 1;
set g = F'' /. x;
A43: dom (F'' /. x) = d by A12, CARD_1:47, CAT_3:45;
A44: F' /. x = F' . x by A12, CARD_1:47, FUNCT_2:def 14
.= (x .--> p2) . x by A20, A42, FUNCT_4:14
.= p2 by A42, FUNCOP_1:13 ;
then cod p2 = (cods F') /. x by A12, CARD_1:47, CAT_3:def 4
.= cod (F'' /. x) by A12, A36, CARD_1:47, CAT_3:def 4 ;
then F'' /. x in Hom d,(cod p2) by A43;
then consider h being Morphism of such that
A45: h in Hom d,c and
A46: for k being Morphism of st k in Hom d,c holds
( ( p1 * k = h' & p2 * k = F'' /. x ) iff h = k ) by A17, A19, A40, CAT_3:def 16;
take h ; :: thesis:
thus h in Hom d,c by A45; :: thesis:
let k be Morphism of ; :: thesis:
assume A47: k in Hom d,c ; :: thesis:
thus ( ( for y being set st y in I holds
(F' /. y) * k = F'' /. y ) implies h = k ) :: thesis:

proof

A48: cod k = c by A47, CAT_1:18;
then A49: cod (p1 * k) = a by A15, A17, CAT_1:42;
assume A50: for y being set st y in I holds
(F' /. y) * k = F'' /. y ; :: thesis:
A51: for y being set st y in I \ {x} holds
(G' /. y) * (p1 * k) = G'' /. y

proof

let y be set ; :: thesis:
assume A52: y in I \ {x} ; :: thesis:
then A53: not y in {x} by XBOOLE_0:def 5;
A54: F' /. y = F' . y by A52, FUNCT_2:def 14
.= (G' * p1) . y by A20, A22, A52, A53, FUNCT_4:def 1
.= (G' * p1) /. y by A52, FUNCT_2:def 14 ;
dom (G' /. y) = a by A52, CAT_3:45;
hence (G' /. y) * (p1 * k) = ((G' /. y) * p1) * k by A15, A17, A48, CAT_1:43
.= ((G' * p1) /. y) * k by A52, CAT_3:def 7
.= F'' /. y by A50, A52, A54
.= F'' . y by A52, FUNCT_2:def 14
.= G'' . y by A52, FUNCT_1:72
.= G'' /. y by A52, FUNCT_2:def 14 ;
:: thesis:

end;

dom k = d by A47, CAT_1:18;
then dom (p1 * k) = d by A15, A48, CAT_1:42;
then p1 * k in Hom d,a by A49;
then A55: p1 * k = h' by A41, A51;
p2 * k = F'' /. x by A12, A44, A50, CARD_1:47;
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

per cases ;

suppose A58: y = x ; :: thesis:

then A59: y in {x} by TARSKI:def 1;
F' /. y = F' . y by A57, FUNCT_2:def 14
.= (x .--> p2) . y by A20, A59, FUNCT_4:14
.= p2 by A59, FUNCOP_1:13 ;
hence (F' /. y) * k = F'' /. y by A46, A47, A56, A58; :: thesis:

end;

suppose A60: y <> x ; :: thesis:

then A61: not y in {x} by TARSKI:def 1;
A62: cod k = c by A47, CAT_1:18;
A63: y in I \ {x} by A57, A60, ZFMISC_1:64;
then A64: dom (G' /. y) = a by CAT_3:45;
F' /. y = F' . y by A57, FUNCT_2:def 14
.= (G' * p1) . y by A20, A22, A57, A61, FUNCT_4:def 1
.= (G' * p1) /. y by A63, FUNCT_2:def 14
.= (G' /. y) * p1 by A63, CAT_3:def 7 ;
hence (F' /. y) * k = (G' /. y) * (p1 * k) by A15, A17, A62, A64, CAT_1:43
.= (G' /. y) * h' by A46, A47, A56
.= G'' /. y by A40, A41, A63
.= G'' . y by A63, FUNCT_2:def 14
.= F'' . y by A63, FUNCT_1:72
.= F'' /. y by A57, FUNCT_2:def 14 ;
:: thesis:

end;

hence (F' /. y) * k = F'' /. y ; :: thesis:

end;

let I be finite set ; :: according to CAT_4:def 3 :: 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:25;
then reconsider F' = {} as Projections_family of a,I by A67, CAT_3:46;
take a ; :: thesis:
take F' ; :: thesis:
for x being set st x in I holds
(cods F') /. x = F /. x ;
hence cods F' = F by CAT_3:1; :: thesis:
thus a is_a_product_wrt F' by A8, A67, CAT_3:55; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A66, A10);
hence ex a being Object of ex F' being Projections_family of a,I st
( cods F' = F & a is_a_product_wrt F' ) by A65; :: thesis: