let I be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: a is terminal

now

thus ( I = {} implies a is terminal ) by A1, Th55; :: thesis: 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; :: thesis: ( Hom b,a <> {} & ex h being Morphism of b,a st
for g being Morphism of b,a holds h = g )
deffunc H₁( 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 = H₁(x) from CAT_3:sch 1();

now

let x be set ; :: thesis: ( x in I implies (doms F9) /. x = (I --> b) /. x )
assume A4: x in I ; :: thesis: (doms F9) /. x = (I --> b) /. x
then A5: cod (F /. x) is terminal by A2;
thus (doms F9) /. x = dom (F9 /. x) by A4, Def3
.= dom (term b,(cod (F /. x))) by A3, A4
.= b by A5, Th39
.= (I --> b) /. x by A4, Th2 ; :: thesis: verum

end;

then doms F9 = I --> b by Th1;
then reconsider F9 = F9 as Projections_family of b,I by Def14;

now

let x be set ; :: thesis: ( x in I implies (cods F) /. x = (cods F9) /. x )
assume A6: x in I ; :: thesis: (cods F) /. x = (cods F9) /. x
then A7: cod (F /. x) is terminal by A2;
thus (cods F) /. x = cod (F /. x) by A6, Def4
.= cod (term b,(cod (F /. x))) by A7, Th39
.= cod (F9 /. x) by A3, A6
.= (cods F9) /. x by A6, Def4 ; :: thesis: verum

end;

then cods F = cods F9 by 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, Def15;
thus Hom b,a <> {} by A8; :: thesis: ex h being Morphism of b,a st
for g being Morphism of b,a holds h = g
reconsider h = h as Morphism of b,a by A8, CAT_1:def 7;
take h = h; :: thesis: for g being Morphism of b,a holds h = g
let g be Morphism of b,a; :: thesis: h = g

now

thus g in Hom b,a by A8, CAT_1:def 7; :: thesis: for x being set st x in I holds
F9 /. x = (F /. x) * g
let x be set ; :: thesis: ( x in I implies F9 /. x = (F /. x) * g )
set c = cod (F /. x);
A10: cod g = a by A8, CAT_1:23;
assume A11: x in I ; :: thesis: F9 /. x = (F /. x) * g
then 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 by CAT_1:def 15;
A13: dom (F /. x) = a by A11, Th45;
then A14: cod ((F /. x) * g) = cod (F /. x) by A10, CAT_1:42;
dom g = b by A8, CAT_1:23;
then dom ((F /. x) * g) = b by A10, A13, CAT_1:42;
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 7;
F9 /. x = term b,(cod (F /. x)) by A3, A11;
hence F9 /. x = f by A12
.= (F /. x) * g by A12, A15 ;
:: thesis: verum

end;

hence h = g by A9; :: thesis: verum

end;

hence a is terminal by CAT_1:def 15; :: thesis: verum