let C be Category; ( C is with_finite_product iff ( 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 ) ) ) )
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 ) ) ) )
( 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 ) ) implies C is with_finite_product )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 )
;
CAT_4:def 2 ( 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 ) ) )
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;
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 )
let a,
b be
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 )
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
;
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 )
take p1 =
F9 /. 0;
ex 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 )
take p2 =
F9 /. 1;
( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 )
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;
( cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 )
(
((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;
c is_a_product_wrt p1,p2
(
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;
verum
end;
given a being Object of C such that A8:
a is terminal
; ( ex a, b being Object of C st
for c being Object of C
for p1, p2 being Morphism of C holds
( not dom p1 = c or not dom p2 = c or not cod p1 = a or not cod p2 = b or not c is_a_product_wrt p1,p2 ) or C is with_finite_product )
defpred S1[ 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 )
; C is with_finite_product
A10:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A11:
S1[
n]
;
S1[n + 1]
let I be
finite set ;
for F being Function of I, the carrier of C st card I = n + 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 )let F be
Function of
I, the
carrier of
C;
( card I = n + 1 implies 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 A12:
card I = n + 1
;
ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
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 for y being object st y in I holds
(doms F9) . y = (I --> c) . ylet y be
object ;
( y in I implies (doms F9) . y = (I --> c) . y )assume A24:
y in I
;
(doms F9) . y = (I --> c) . ynow (I --> c) . y = (doms F9) /. yper cases
( y = the Element of I or y <> the Element of I )
;
suppose A26:
y <> the
Element of
I
;
(doms F9) /. y = (I --> c) . ythen 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
;
verum end; end; end; hence
(doms F9) . y = (I --> c) . y
by A24, FUNCT_2:def 13;
verum end;
then reconsider F9 =
F9 as
Projections_family of
c,
I by CAT_3:def 13, FUNCT_2:12;
take
c
;
ex F9 being Projections_family of c,I st
( cods F9 = F & c is_a_product_wrt F9 )
take
F9
;
( cods F9 = F & c is_a_product_wrt F9 )
A29:
now for y being set st y in I holds
(cods F9) /. y = F /. ylet y be
set ;
( y in I implies (cods F9) /. y = F /. y )assume A30:
y in I
;
(cods F9) /. y = F /. ynow (cods F9) /. y = F /. yper cases
( y = the Element of I or y <> the Element of I )
;
suppose A33:
y <> the
Element of
I
;
(cods F9) /. y = F /. ythen 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
;
verum end; end; end; hence
(cods F9) /. y = F /. y
;
verum end;
hence
cods F9 = F
by CAT_3:1;
c is_a_product_wrt F9
thus
F9 is
Projections_family of
c,
I
;
CAT_3:def 14 for b1 being Element of the carrier of C
for b2 being Projections_family of b1,I holds
( not cods F9 = cods b2 or ex b3 being Element of the carrier' of C st
( b3 in Hom (b1,c) & ( for b4 being Element of the carrier' of C holds
( not b4 in Hom (b1,c) or ( ( ex b5 being set st
( b5 in I & not (F9 /. b5) (*) b4 = b2 /. b5 ) or b3 = b4 ) & ( not b3 = b4 or for b5 being set holds
( not b5 in I or (F9 /. b5) (*) b4 = b2 /. b5 ) ) ) ) ) ) )
let d be
Object of
C;
for b1 being Projections_family of d,I holds
( not cods F9 = cods b1 or ex b2 being Element of the carrier' of C st
( b2 in Hom (d,c) & ( for b3 being Element of the carrier' of C holds
( not b3 in Hom (d,c) or ( ( ex b4 being set st
( b4 in I & not (F9 /. b4) (*) b3 = b1 /. b4 ) or b2 = b3 ) & ( not b2 = b3 or for b4 being set holds
( not b4 in I or (F9 /. b4) (*) b3 = b1 /. b4 ) ) ) ) ) ) )let F99 be
Projections_family of
d,
I;
( not cods F9 = cods F99 or ex b1 being Element of the carrier' of C st
( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (d,c) or ( ( ex b3 being set st
( b3 in I & not (F9 /. b3) (*) b2 = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or (F9 /. b3) (*) b2 = F99 /. b3 ) ) ) ) ) ) )
assume A36:
cods F9 = cods F99
;
ex b1 being Element of the carrier' of C st
( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (d,c) or ( ( ex b3 being set st
( b3 in I & not (F9 /. b3) (*) b2 = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or (F9 /. b3) (*) b2 = F99 /. b3 ) ) ) ) ) )
reconsider G99 =
F99 | (I \ { the Element of I}) as
Function of
(I \ { the Element of I}), the
carrier' of
C by FUNCT_2:32;
then reconsider G99 =
G99 as
Projections_family of
d,
I \ { the Element of I} by CAT_3:1, CAT_3:def 13;
now for y being set st y in I \ { the Element of I} holds
(cods G9) /. y = (cods G99) /. ylet y be
set ;
( y in I \ { the Element of I} implies (cods G9) /. y = (cods G99) /. y )assume A38:
y in I \ { the Element of I}
;
(cods G9) /. y = (cods G99) /. ythen 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
;
verum 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
;
( h in Hom (d,c) & ( for b1 being Element of the carrier' of C holds
( not b1 in Hom (d,c) or ( ( ex b2 being set st
( b2 in I & not (F9 /. b2) (*) b1 = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or (F9 /. b2) (*) b1 = F99 /. b2 ) ) ) ) ) )
thus
h in Hom (
d,
c)
by A45;
for b1 being Element of the carrier' of C holds
( not b1 in Hom (d,c) or ( ( ex b2 being set st
( b2 in I & not (F9 /. b2) (*) b1 = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or (F9 /. b2) (*) b1 = F99 /. b2 ) ) ) )
let k be
Morphism of
C;
( not k in Hom (d,c) or ( ( ex b1 being set st
( b1 in I & not (F9 /. b1) (*) k = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) ) ) )
assume A47:
k in Hom (
d,
c)
;
( ( ex b1 being set st
( b1 in I & not (F9 /. b1) (*) k = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) ) )
thus
( ( for
y being
set st
y in I holds
(F9 /. y) (*) k = F99 /. y ) implies
h = k )
( not h = k or for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) )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
;
h = k
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 ;
( y in I \ { the Element of I} implies (G9 /. y) (*) (p1 (*) k) = G99 /. y )
assume A52:
y in I \ { the Element of I}
;
(G9 /. y) (*) (p1 (*) k) = G99 /. y
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
;
verum
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;
verum
end;
assume A56:
h = k
;
for b1 being set holds
( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 )
let y be
set ;
( not y in I or (F9 /. y) (*) k = F99 /. y )
assume A57:
y in I
;
(F9 /. y) (*) k = F99 /. y
now (F9 /. y) (*) k = F99 /. yper cases
( y = the Element of I or y <> the Element of I )
;
suppose A60:
y <> the
Element of
I
;
(F9 /. y) (*) k = F99 /. ythen 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
;
verum end; end; end;
hence
(F9 /. y) (*) k = F99 /. y
;
verum
end;
let I be finite set ; CAT_4:def 2 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 )
let F be 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 )
A65:
card I = card I
;
A66:
S1[ 0 ]
proof
let I be
finite set ;
for F being Function of I, the carrier of C st card I = 0 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 )let F be
Function of
I, the
carrier of
C;
( card I = 0 implies 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
card I = 0
;
ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
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
;
ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 )
take
F9
;
( cods F9 = F & a is_a_product_wrt F9 )
for
x being
set st
x in I holds
(cods F9) /. x = F /. x
;
hence
cods F9 = F
by CAT_3:1;
a is_a_product_wrt F9
thus
a is_a_product_wrt F9
by A8, A67, CAT_3:50;
verum
end;
for n being Nat holds S1[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; verum