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

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 :: thesis: ( ( 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 ) ) )

hence
a is terminal
; :: thesis: verum( 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; :: 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_{1}( 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_{1}(x)
from CAT_3:sch 1();

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; :: 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 5;

take h = h; :: thesis: for g being Morphism of b,a holds h = g

let g be Morphism of b,a; :: thesis: h = g

end;( 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

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

now :: thesis: for x being set st x in I holds

(doms F9) /. x = (I --> b) /. x

then reconsider F9 = F9 as Projections_family of b,I by Def13, Th1;(doms F9) /. x = (I --> b) /. x

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, Def1

.= dom (term (b,(cod (F /. x)))) by A3, A4

.= b by A5, Th35

.= (I --> b) /. x by A4, Th2 ; :: thesis: verum

end;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, Def1

.= dom (term (b,(cod (F /. x)))) by A3, A4

.= b by A5, Th35

.= (I --> b) /. x by A4, Th2 ; :: thesis: verum

now :: thesis: for x being set st x in I holds

(cods F) /. x = (cods F9) /. x

then consider h being Morphism of C such that (cods F) /. x = (cods F9) /. x

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, Def2

.= cod (term (b,(cod (F /. x)))) by A7, Th35

.= cod (F9 /. x) by A3, A6

.= (cods F9) /. x by A6, Def2 ; :: thesis: verum

end;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, Def2

.= cod (term (b,(cod (F /. x)))) by A7, Th35

.= cod (F9 /. x) by A3, A6

.= (cods F9) /. x by A6, Def2 ; :: thesis: verum

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; :: 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 5;

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 :: thesis: ( g in Hom (b,a) & ( for x being set st x in I holds

F9 /. x = (F /. x) (*) g ) )

hence
h = g
by A9; :: thesis: verumF9 /. x = (F /. x) (*) g ) )

thus
g in Hom (b,a)
by A8, CAT_1:def 5; :: 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:5;

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 ;

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 ;

:: thesis: verum

end;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:5;

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 ;

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 ;

:: thesis: verum