let C be Category; :: thesis:
let a be Object of C; :: thesis:
let F be Injections_family of a, {} ; :: thesis:
thus ( a is_a_coproduct_wrt F implies a is initial ) :: thesis:

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

end;

assume A5: a is initial ; :: thesis:
thus F is Injections_family of a, {} ; :: according to CAT_3:def 18 :: thesis:
let b be Object of C; :: thesis:
consider h being Morphism of a,b such that
A6: for g being Morphism of a,b holds h = g by A5, CAT_1:def 16;
let F9 be Injections_family of b, {} ; :: thesis:
assume doms F = doms F9 ; :: thesis:
take h ; :: thesis:
Hom a,b <> {} by A5, CAT_1:def 16;
hence h in Hom a,b by CAT_1:def 7; :: thesis:
let k be Morphism of C; :: thesis:
assume k in Hom a,b ; :: thesis:
then k is Morphism of a,b by CAT_1:def 7;
hence ( ( for x being set st x in {} holds
k * (F /. x) = F9 /. x ) iff h = k ) by A6; :: thesis: