let I be set ; for C being Category
for a being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds
cod (F /. x) is terminal ) holds
a is terminal
let C be Category; for a being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds
cod (F /. x) is terminal ) holds
a is terminal
let a be Object of C; for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds
cod (F /. x) is terminal ) holds
a is terminal
let F be Projections_family of a,I; ( a is_a_product_wrt F & ( for x being set st x in I holds
cod (F /. x) is terminal ) implies a is terminal )
assume that
A1:
a is_a_product_wrt F
and
A2:
for x being set st x in I holds
cod (F /. x) is terminal
; a is terminal
now ( ( I = {} implies a is terminal ) & ( for b being Object of C holds
( Hom (b,a) <> {} & ex h being Morphism of b,a st
for g being Morphism of b,a holds h = g ) ) )thus
(
I = {} implies
a is
terminal )
by A1, Th50;
for b being Object of C holds
( Hom (b,a) <> {} & ex h being Morphism of b,a st
for g being Morphism of b,a holds h = g )let b be
Object of
C;
( Hom (b,a) <> {} & ex h being Morphism of b,a st
for g being Morphism of b,a holds h = g )deffunc H1(
set )
-> Morphism of
b,
cod (F /. $1) =
term (
b,
(cod (F /. $1)));
consider F9 being
Function of
I, the
carrier' of
C such that A3:
for
x being
set st
x in I holds
F9 /. x = H1(
x)
from CAT_3:sch 1();
then reconsider F9 =
F9 as
Projections_family of
b,
I by Def13, Th1;
then consider h being
Morphism of
C such that A8:
h in Hom (
b,
a)
and A9:
for
k being
Morphism of
C st
k in Hom (
b,
a) holds
( ( for
x being
set st
x in I holds
(F /. x) (*) k = F9 /. x ) iff
h = k )
by A1, Th1;
thus
Hom (
b,
a)
<> {}
by A8;
ex h being Morphism of b,a st
for g being Morphism of b,a holds h = greconsider h =
h as
Morphism of
b,
a by A8, CAT_1:def 5;
take h =
h;
for g being Morphism of b,a holds h = glet g be
Morphism of
b,
a;
h = gnow ( g in Hom (b,a) & ( for x being set st x in I holds
F9 /. x = (F /. x) (*) g ) )thus
g in Hom (
b,
a)
by A8, CAT_1:def 5;
for x being set st x in I holds
F9 /. x = (F /. x) (*) glet x be
set ;
( x in I implies F9 /. x = (F /. x) (*) g )set c =
cod (F /. x);
A10:
cod g = a
by A8, CAT_1:5;
assume A11:
x in I
;
F9 /. x = (F /. x) (*) gthen
cod (F /. x) is
terminal
by A2;
then consider f being
Morphism of
b,
cod (F /. x) such that A12:
for
f9 being
Morphism of
b,
cod (F /. x) holds
f = f9
;
A13:
dom (F /. x) = a
by A11, Th41;
then A14:
cod ((F /. x) (*) g) = cod (F /. x)
by A10, CAT_1:17;
dom g = b
by A8, CAT_1:5;
then
dom ((F /. x) (*) g) = b
by A10, A13, CAT_1:17;
then
(F /. x) (*) g in Hom (
b,
(cod (F /. x)))
by A14;
then A15:
(F /. x) (*) g is
Morphism of
b,
cod (F /. x)
by CAT_1:def 5;
F9 /. x = term (
b,
(cod (F /. x)))
by A3, A11;
hence F9 /. x =
f
by A12
.=
(F /. x) (*) g
by A12, A15
;
verum end; hence
h = g
by A9;
verum end;
hence
a is terminal
; verum