let C be Category; :: thesis:
let a, c, b be Object of C; :: thesis:
assume A1: ( Hom a,c <> {} & Hom b,c <> {} ) ; :: thesis:
let i1 be Morphism of a,c; :: thesis:
let i2 be Morphism of b,c; :: thesis:
thus ( c is_a_coproduct_wrt i1,i2 implies for d being Object of C st Hom a,d <> {} & Hom b,d <> {} holds
( Hom c,d <> {} & ( for f being Morphism of a,d
for g being Morphism of b,d ex h being Morphism of c,d st
for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) ) :: thesis:

assume that
( cod i1 = c & cod i2 = c ) and
A2: for d being Object of C
for f, g being Morphism of C st f in Hom (dom i1),d & g in Hom (dom i2),d holds
ex h being Morphism of C st
( h in Hom c,d & ( for k being Morphism of C st k in Hom c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) ; :: according to CAT_3:def 19 :: thesis:
let d be Object of C; :: thesis:
assume A3: ( Hom a,d <> {} & Hom b,d <> {} ) ; :: thesis:
consider f being Morphism of a,d, g being Morphism of b,d;
A4: ( dom i1 = a & dom i2 = b ) by A1, CAT_1:23;
then ( f in Hom (dom i1),d & g in Hom (dom i2),d ) by A3, CAT_1:def 7;
then A5: ex h being Morphism of C st
( h in Hom c,d & ( for k being Morphism of C st k in Hom c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) by A2;
hence Hom c,d <> {} ; :: thesis:
let f be Morphism of a,d; :: thesis:
let g be Morphism of b,d; :: thesis:
( f in Hom (dom i1),d & g in Hom (dom i2),d ) by A3, A4, CAT_1:def 7;
then consider h being Morphism of C such that
A6: h in Hom c,d and
A7: for k being Morphism of C st k in Hom c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) by A2;
reconsider h = h as Morphism of c,d by A6, CAT_1:def 7;
take h ; :: thesis:
let k be Morphism of c,d; :: thesis:
( k * i1 = k * i1 & k * i2 = k * i2 & k in Hom c,d ) by A1, A5, CAT_1:def 7, CAT_1:def 13;
hence ( ( k * i1 = f & k * i2 = g ) iff h = k ) by A7; :: thesis:

end;

assume A8: for d being Object of C st Hom a,d <> {} & Hom b,d <> {} holds
( Hom c,d <> {} & ( for f being Morphism of a,d
for g being Morphism of b,d ex h being Morphism of c,d st
for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) ; :: thesis:
thus ( cod i1 = c & cod i2 = c ) by A1, CAT_1:23; :: according to CAT_3:def 19 :: thesis:
let d be Object of C; :: thesis:
let f, g be Morphism of C; :: thesis:
assume that
A9: f in Hom (dom i1),d and
A10: g in Hom (dom i2),d ; :: thesis:
A11: ( dom i1 = a & dom i2 = b ) by A1, CAT_1:23;
then ( f is Morphism of a,d & g is Morphism of b,d & Hom a,d <> {} & Hom b,d <> {} ) by A9, A10, CAT_1:def 7;
then consider h being Morphism of c,d such that
A12: for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) by A8;
reconsider h' = h as Morphism of C ;
take h' ; :: thesis:
A13: Hom c,d <> {} by A8, A9, A10, A11;
hence h' in Hom c,d by CAT_1:def 7; :: thesis:
let k be Morphism of C; :: thesis:
assume k in Hom c,d ; :: thesis:
then reconsider k' = k as Morphism of c,d by CAT_1:def 7;
( k * i1 = k' * i1 & k * i2 = k' * i2 ) by A1, A13, CAT_1:def 13;
hence ( ( k * i1 = f & k * i2 = g ) iff h' = k ) by A12; :: thesis: