let C be Category; :: thesis: for a, b, c being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds

for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

let a, b, c be Object of C; :: thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} implies for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) ) )

assume that

A1: Hom (a,c) <> {} and

A2: Hom (b,c) <> {} ; :: thesis: for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

let i1 be Morphism of a,c; :: thesis: for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

let i2 be Morphism of b,c; :: thesis: ( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

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: ( ( 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 ) ) ) ) implies c is_a_coproduct_wrt i1,i2 )

( 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: c is_a_coproduct_wrt i1,i2

thus ( cod i1 = c & cod i2 = c ) by A1, A2, CAT_1:5; :: according to CAT_3:def 18 :: thesis: 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 ) ) )

let d be Object of C; :: thesis: 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 ) ) )

let f, g be Morphism of C; :: thesis: ( f in Hom ((dom i1),d) & g in Hom ((dom i2),d) implies 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 ) ) ) )

assume that

A15: f in Hom ((dom i1),d) and

A16: g in Hom ((dom i2),d) ; :: thesis: 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 ) ) )

A17: Hom (a,d) <> {} by A1, A15, CAT_1:5;

A18: dom i1 = a by A1, CAT_1:5;

then A19: f is Morphism of a,d by A15, CAT_1:def 5;

A20: dom i2 = b by A2, CAT_1:5;

then g is Morphism of b,d by A16, CAT_1:def 5;

then consider h being Morphism of c,d such that

A21: for k being Morphism of c,d holds

( ( k * i1 = f & k * i2 = g ) iff h = k ) by A14, A16, A20, A19, A17;

reconsider h9 = h as Morphism of C ;

take h9 ; :: thesis: ( h9 in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) ) )

A22: Hom (c,d) <> {} by A14, A15, A16, A18, A20;

hence h9 in Hom (c,d) by CAT_1:def 5; :: thesis: for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k )

let k be Morphism of C; :: thesis: ( k in Hom (c,d) implies ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) )

assume k in Hom (c,d) ; :: thesis: ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k )

then reconsider k9 = k as Morphism of c,d by CAT_1:def 5;

( k (*) i1 = k9 * i1 & k (*) i2 = k9 * i2 ) by A1, A2, A22, CAT_1:def 13;

hence ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) by A21; :: thesis: verum

for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

let a, b, c be Object of C; :: thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} implies for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) ) )

assume that

A1: Hom (a,c) <> {} and

A2: Hom (b,c) <> {} ; :: thesis: for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

let i1 be Morphism of a,c; :: thesis: for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

let i2 be Morphism of b,c; :: thesis: ( c is_a_coproduct_wrt i1,i2 iff 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 ) ) ) )

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: ( ( 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 ) ) ) ) implies c is_a_coproduct_wrt i1,i2 )

proof

assume A14:
for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
assume that

cod i1 = c and

cod i2 = c and

A3: 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 18 :: thesis: 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 ) ) )

let d be Object of C; :: thesis: ( Hom (a,d) <> {} & Hom (b,d) <> {} implies ( 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 ) ) ) )

assume that

A4: Hom (a,d) <> {} and

A5: Hom (b,d) <> {} ; :: thesis: ( 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 ) ) )

set f = the Morphism of a,d;

set g = the Morphism of b,d;

A6: dom i2 = b by A2, CAT_1:5;

then A7: the Morphism of b,d in Hom ((dom i2),d) by A5, CAT_1:def 5;

A8: dom i1 = a by A1, CAT_1:5;

then the Morphism of a,d in Hom ((dom i1),d) by A4, CAT_1:def 5;

then A9: 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 = the Morphism of a,d & k (*) i2 = the Morphism of b,d ) iff h = k ) ) ) by A3, A7;

hence Hom (c,d) <> {} ; :: thesis: 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 )

let f be Morphism of a,d; :: thesis: 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 )

let g be Morphism of b,d; :: thesis: 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 )

A10: g in Hom ((dom i2),d) by A5, A6, CAT_1:def 5;

f in Hom ((dom i1),d) by A4, A8, CAT_1:def 5;

then consider h being Morphism of C such that

A11: h in Hom (c,d) and

A12: for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) by A3, A10;

reconsider h = h as Morphism of c,d by A11, CAT_1:def 5;

take h ; :: thesis: for k being Morphism of c,d holds

( ( k * i1 = f & k * i2 = g ) iff h = k )

let k be Morphism of c,d; :: thesis: ( ( k * i1 = f & k * i2 = g ) iff h = k )

A13: k in Hom (c,d) by A9, CAT_1:def 5;

( k * i1 = k (*) i1 & k * i2 = k (*) i2 ) by A1, A2, A9, CAT_1:def 13;

hence ( ( k * i1 = f & k * i2 = g ) iff h = k ) by A12, A13; :: thesis: verum

end;cod i1 = c and

cod i2 = c and

A3: 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 18 :: thesis: 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 ) ) )

let d be Object of C; :: thesis: ( Hom (a,d) <> {} & Hom (b,d) <> {} implies ( 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 ) ) ) )

assume that

A4: Hom (a,d) <> {} and

A5: Hom (b,d) <> {} ; :: thesis: ( 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 ) ) )

set f = the Morphism of a,d;

set g = the Morphism of b,d;

A6: dom i2 = b by A2, CAT_1:5;

then A7: the Morphism of b,d in Hom ((dom i2),d) by A5, CAT_1:def 5;

A8: dom i1 = a by A1, CAT_1:5;

then the Morphism of a,d in Hom ((dom i1),d) by A4, CAT_1:def 5;

then A9: 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 = the Morphism of a,d & k (*) i2 = the Morphism of b,d ) iff h = k ) ) ) by A3, A7;

hence Hom (c,d) <> {} ; :: thesis: 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 )

let f be Morphism of a,d; :: thesis: 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 )

let g be Morphism of b,d; :: thesis: 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 )

A10: g in Hom ((dom i2),d) by A5, A6, CAT_1:def 5;

f in Hom ((dom i1),d) by A4, A8, CAT_1:def 5;

then consider h being Morphism of C such that

A11: h in Hom (c,d) and

A12: for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) by A3, A10;

reconsider h = h as Morphism of c,d by A11, CAT_1:def 5;

take h ; :: thesis: for k being Morphism of c,d holds

( ( k * i1 = f & k * i2 = g ) iff h = k )

let k be Morphism of c,d; :: thesis: ( ( k * i1 = f & k * i2 = g ) iff h = k )

A13: k in Hom (c,d) by A9, CAT_1:def 5;

( k * i1 = k (*) i1 & k * i2 = k (*) i2 ) by A1, A2, A9, CAT_1:def 13;

hence ( ( k * i1 = f & k * i2 = g ) iff h = k ) by A12, A13; :: thesis: verum

( 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: c is_a_coproduct_wrt i1,i2

thus ( cod i1 = c & cod i2 = c ) by A1, A2, CAT_1:5; :: according to CAT_3:def 18 :: thesis: 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 ) ) )

let d be Object of C; :: thesis: 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 ) ) )

let f, g be Morphism of C; :: thesis: ( f in Hom ((dom i1),d) & g in Hom ((dom i2),d) implies 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 ) ) ) )

assume that

A15: f in Hom ((dom i1),d) and

A16: g in Hom ((dom i2),d) ; :: thesis: 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 ) ) )

A17: Hom (a,d) <> {} by A1, A15, CAT_1:5;

A18: dom i1 = a by A1, CAT_1:5;

then A19: f is Morphism of a,d by A15, CAT_1:def 5;

A20: dom i2 = b by A2, CAT_1:5;

then g is Morphism of b,d by A16, CAT_1:def 5;

then consider h being Morphism of c,d such that

A21: for k being Morphism of c,d holds

( ( k * i1 = f & k * i2 = g ) iff h = k ) by A14, A16, A20, A19, A17;

reconsider h9 = h as Morphism of C ;

take h9 ; :: thesis: ( h9 in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) ) )

A22: Hom (c,d) <> {} by A14, A15, A16, A18, A20;

hence h9 in Hom (c,d) by CAT_1:def 5; :: thesis: for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k )

let k be Morphism of C; :: thesis: ( k in Hom (c,d) implies ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) )

assume k in Hom (c,d) ; :: thesis: ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k )

then reconsider k9 = k as Morphism of c,d by CAT_1:def 5;

( k (*) i1 = k9 * i1 & k (*) i2 = k9 * i2 ) by A1, A2, A22, CAT_1:def 13;

hence ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) by A21; :: thesis: verum