let C be Category; :: thesis: for a being Object of C

for F being Injections_family of a, {} holds

( a is_a_coproduct_wrt F iff a is initial )

let a be Object of C; :: thesis: for F being Injections_family of a, {} holds

( a is_a_coproduct_wrt F iff a is initial )

let F be Injections_family of a, {} ; :: thesis: ( a is_a_coproduct_wrt F iff a is initial )

thus ( a is_a_coproduct_wrt F implies a is initial ) :: thesis: ( a is initial implies a is_a_coproduct_wrt F )

thus F is Injections_family of a, {} ; :: according to CAT_3:def 17 :: thesis: for d being Object of C

for F9 being Injections_family of d, {} st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,d) & ( for k being Morphism of C st k in Hom (a,d) holds

( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Injections_family of b, {} st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,b) & ( 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 ) ) )

consider h being Morphism of a,b such that

A6: for g being Morphism of a,b holds h = g by A5;

let F9 be Injections_family of b, {} ; :: thesis: ( doms F = doms F9 implies ex h being Morphism of C st

( h in Hom (a,b) & ( 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 ) ) ) )

assume doms F = doms F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (a,b) & ( 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 ) ) )

take h ; :: thesis: ( h in Hom (a,b) & ( 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 ) ) )

Hom (a,b) <> {} by A5;

hence h in Hom (a,b) by CAT_1:def 5; :: thesis: 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 )

let k be Morphism of C; :: thesis: ( k in Hom (a,b) implies ( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k ) )

assume k in Hom (a,b) ; :: thesis: ( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k )

then k is Morphism of a,b by CAT_1:def 5;

hence ( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k ) by A6; :: thesis: verum

for F being Injections_family of a, {} holds

( a is_a_coproduct_wrt F iff a is initial )

let a be Object of C; :: thesis: for F being Injections_family of a, {} holds

( a is_a_coproduct_wrt F iff a is initial )

let F be Injections_family of a, {} ; :: thesis: ( a is_a_coproduct_wrt F iff a is initial )

thus ( a is_a_coproduct_wrt F implies a is initial ) :: thesis: ( a is initial implies a is_a_coproduct_wrt F )

proof

assume A5:
a is initial
; :: thesis: a is_a_coproduct_wrt F
assume A1:
a is_a_coproduct_wrt F
; :: thesis: a is initial

let b be Object of C; :: according to CAT_1:def 19 :: thesis: ( not Hom (a,b) = {} & ex b_{1} being Morphism of a,b st

for b_{2} being Morphism of a,b holds b_{1} = b_{2} )

set F9 = the Injections_family of b, {} ;

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) = the Injections_family of b, {} /. x ) iff h = k ) by A1;

thus Hom (a,b) <> {} by A2; :: thesis: ex b_{1} being Morphism of a,b st

for b_{2} being Morphism of a,b holds b_{1} = b_{2}

reconsider f = h as Morphism of a,b by A2, CAT_1:def 5;

take f ; :: thesis: for b_{1} being Morphism of a,b holds f = b_{1}

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

A4: for x being set st x in {} holds

g (*) (F /. x) = the Injections_family of b, {} /. x ;

g in Hom (a,b) by A2, CAT_1:def 5;

hence f = g by A3, A4; :: thesis: verum

end;let b be Object of C; :: according to CAT_1:def 19 :: thesis: ( not Hom (a,b) = {} & ex b

for b

set F9 = the Injections_family of b, {} ;

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) = the Injections_family of b, {} /. x ) iff h = k ) by A1;

thus Hom (a,b) <> {} by A2; :: thesis: ex b

for b

reconsider f = h as Morphism of a,b by A2, CAT_1:def 5;

take f ; :: thesis: for b

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

A4: for x being set st x in {} holds

g (*) (F /. x) = the Injections_family of b, {} /. x ;

g in Hom (a,b) by A2, CAT_1:def 5;

hence f = g by A3, A4; :: thesis: verum

thus F is Injections_family of a, {} ; :: according to CAT_3:def 17 :: thesis: for d being Object of C

for F9 being Injections_family of d, {} st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,d) & ( for k being Morphism of C st k in Hom (a,d) holds

( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Injections_family of b, {} st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,b) & ( 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 ) ) )

consider h being Morphism of a,b such that

A6: for g being Morphism of a,b holds h = g by A5;

let F9 be Injections_family of b, {} ; :: thesis: ( doms F = doms F9 implies ex h being Morphism of C st

( h in Hom (a,b) & ( 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 ) ) ) )

assume doms F = doms F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (a,b) & ( 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 ) ) )

take h ; :: thesis: ( h in Hom (a,b) & ( 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 ) ) )

Hom (a,b) <> {} by A5;

hence h in Hom (a,b) by CAT_1:def 5; :: thesis: 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 )

let k be Morphism of C; :: thesis: ( k in Hom (a,b) implies ( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k ) )

assume k in Hom (a,b) ; :: thesis: ( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k )

then k is Morphism of a,b by CAT_1:def 5;

hence ( ( for x being set st x in {} holds

k (*) (F /. x) = F9 /. x ) iff h = k ) by A6; :: thesis: verum