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

assume A1: a is_a_product_wrt F ; :: thesis:
let b be Object of ; :: according to CAT_1:def 15 :: thesis:
consider F' being Projections_family of b, {} ;
cods F = {} ;
then consider h being Morphism of such that
A2: h in Hom b,a and
A3: for k being Morphism of st k in Hom b,a holds
( ( for x being set st x in {} holds
(F /. x) * k = F' /. x ) iff h = k ) by A1, Def15;
thus Hom b,a <> {} by A2; :: thesis:
reconsider f = h as Morphism of b,a by A2, CAT_1:def 7;
take f ; :: thesis:
let g be Morphism of b,a; :: thesis:
A4: for x being set st x in {} holds
(F /. x) * g = F' /. x ;
g in Hom b,a by A2, CAT_1:def 7;
hence f = g by A3, A4; :: thesis:

end;

assume A5: a is terminal ; :: thesis:
thus F is Projections_family of a, {} by Th46; :: according to CAT_3:def 15 :: thesis:
let b be Object of ; :: thesis:
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 15;
let F' be Projections_family of b, {} ; :: thesis:
assume cods F = cods F' ; :: thesis:
take h ; :: thesis:
Hom b,a <> {} by A5, CAT_1:def 15;
hence h in Hom b,a by CAT_1:def 7; :: thesis:
let k be Morphism of ; :: thesis:
assume k in Hom b,a ; :: thesis:
then k is Morphism of b,a by CAT_1:def 7;
hence ( ( for x being set st x in {} holds
(F /. x) * k = F' /. x ) iff h = k ) by A6; :: thesis: