let C be Category; :: thesis: for a being Object of C
for F being Function of {}, the carrier' of C holds
( a is_a_product_wrt F iff a is terminal )
let a be Object of C; :: thesis: for F being Function of {}, the carrier' of C holds
( a is_a_product_wrt F iff a is terminal )
let F be Function of {}, the carrier' of C; :: thesis: ( a is_a_product_wrt F iff a is terminal )
thus ( a is_a_product_wrt F implies a is terminal ) :: thesis: ( a is terminal implies a is_a_product_wrt F )

proof

assume A1: a is_a_product_wrt F ; :: thesis: a is terminal
let b be Object of C; :: according to CAT_1:def 12 :: thesis: ( not Hom (b,a) = {} & ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂ )
set F9 = the Projections_family of b, {} ;
cods F = {} ;
then consider h being Morphism of C such that
A2: h in Hom (b,a) and
A3: for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in {} holds
(F /. x) * k = the Projections_family of b, {} /. x ) iff h = k ) by A1, Def15;
thus Hom (b,a) <> {} by A2; :: thesis: ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂
reconsider f = h as Morphism of b,a by A2, CAT_1:def 4;
take f ; :: thesis: for b₁ being Morphism of b,a holds f = b₁
let g be Morphism of b,a; :: thesis: f = g
A4: for x being set st x in {} holds
(F /. x) * g = the Projections_family of b, {} /. x ;
g in Hom (b,a) by A2, CAT_1:def 4;
hence f = g by A3, A4; :: thesis: verum

end;

assume A5: a is terminal ; :: thesis: a is_a_product_wrt F
thus F is Projections_family of a, {} by Th46; :: according to CAT_3:def 13 :: thesis: for b being Object of C
for F9 being Projections_family of b, {} st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k ) ) )
let b be Object of C; :: thesis: for F9 being Projections_family of b, {} st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k ) ) )
consider h being Morphism of b,a such that
A6: for g being Morphism of b,a holds h = g by A5, CAT_1:def 12;
let F9 be Projections_family of b, {} ; :: thesis: ( cods F = cods F9 implies ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k ) ) ) )
assume cods F = cods F9 ; :: thesis: ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k ) ) )
take h ; :: thesis: ( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k ) ) )
Hom (b,a) <> {} by A5, CAT_1:def 12;
hence h in Hom (b,a) by CAT_1:def 4; :: thesis: for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k )
let k be Morphism of C; :: thesis: ( k in Hom (b,a) implies ( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k ) )
assume k in Hom (b,a) ; :: thesis: ( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k )
then k is Morphism of b,a by CAT_1:def 4;
hence ( ( for x being set st x in {} holds
(F /. x) * k = F9 /. x ) iff h = k ) by A6; :: thesis: verum