let x1, x2 be set ; :: thesis: for C being Category

for c being Object of C

for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

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

for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

let c be Object of C; :: thesis: for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

let i1, i2 be Morphism of C; :: thesis: ( x1 <> x2 implies ( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) ) )

set F = (x1,x2) --> (i1,i2);

set I = {x1,x2};

assume A1: x1 <> x2 ; :: thesis: ( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

thus ( c is_a_coproduct_wrt i1,i2 implies c is_a_coproduct_wrt (x1,x2) --> (i1,i2) ) :: thesis: ( c is_a_coproduct_wrt (x1,x2) --> (i1,i2) implies c is_a_coproduct_wrt i1,i2 )

then A16: (x1,x2) --> (i1,i2) is Injections_family of c,{x1,x2} ;

x2 in {x1,x2} by TARSKI:def 2;

then A17: cod (((x1,x2) --> (i1,i2)) /. x2) = c by A16, Th62;

x1 in {x1,x2} by TARSKI:def 2;

then cod (((x1,x2) --> (i1,i2)) /. x1) = c by A16, Th62;

hence ( cod i1 = c & cod i2 = c ) by A1, A17, Th3; :: 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

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

A19: 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 ) ) )

( cod f = d & cod g = d ) by A18, A19, CAT_1:1;

then reconsider F9 = (x1,x2) --> (f,g) as Injections_family of d,{x1,x2} by Th65;

doms ((x1,x2) --> (i1,i2)) = (x1,x2) --> ((dom i1),(dom i2)) by Th6

.= (x1,x2) --> ((dom f),(dom i2)) by A18, CAT_1:1

.= (x1,x2) --> ((dom f),(dom g)) by A19, CAT_1:1

.= doms F9 by Th6 ;

then consider h being Morphism of C such that

A20: h in Hom (c,d) and

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

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) by A15;

take h ; :: thesis: ( 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 ) ) )

thus h in Hom (c,d) by A20; :: thesis: for k being Morphism of C st k in Hom (c,d) holds

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

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

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

thus ( k (*) i1 = f & k (*) i2 = g implies h = k ) :: thesis: ( h = k implies ( k (*) i1 = f & k (*) i2 = g ) )

x2 in {x1,x2} by TARSKI:def 2;

then k (*) (((x1,x2) --> (i1,i2)) /. x2) = F9 /. x2 by A21, A22, A24;

then A25: k (*) (((x1,x2) --> (i1,i2)) /. x2) = g by A1, Th3;

x1 in {x1,x2} by TARSKI:def 2;

then k (*) (((x1,x2) --> (i1,i2)) /. x1) = F9 /. x1 by A21, A22, A24;

then k (*) (((x1,x2) --> (i1,i2)) /. x1) = f by A1, Th3;

hence ( k (*) i1 = f & k (*) i2 = g ) by A1, A25, Th3; :: thesis: verum

for c being Object of C

for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

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

for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

let c be Object of C; :: thesis: for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

let i1, i2 be Morphism of C; :: thesis: ( x1 <> x2 implies ( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) ) )

set F = (x1,x2) --> (i1,i2);

set I = {x1,x2};

assume A1: x1 <> x2 ; :: thesis: ( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

thus ( c is_a_coproduct_wrt i1,i2 implies c is_a_coproduct_wrt (x1,x2) --> (i1,i2) ) :: thesis: ( c is_a_coproduct_wrt (x1,x2) --> (i1,i2) implies c is_a_coproduct_wrt i1,i2 )

proof

assume A15:
c is_a_coproduct_wrt (x1,x2) --> (i1,i2)
; :: thesis: c is_a_coproduct_wrt i1,i2
assume A2:
c is_a_coproduct_wrt i1,i2
; :: thesis: c is_a_coproduct_wrt (x1,x2) --> (i1,i2)

then ( cod i1 = c & cod i2 = c ) ;

hence (x1,x2) --> (i1,i2) is Injections_family of c,{x1,x2} by Th65; :: according to CAT_3:def 17 :: thesis: for d being Object of C

for F9 being Injections_family of d,{x1,x2} st doms ((x1,x2) --> (i1,i2)) = doms F9 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

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Injections_family of b,{x1,x2} st doms ((x1,x2) --> (i1,i2)) = doms F9 holds

ex h being Morphism of C st

( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

let F9 be Injections_family of b,{x1,x2}; :: thesis: ( doms ((x1,x2) --> (i1,i2)) = doms F9 implies ex h being Morphism of C st

( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) ) )

assume A3: doms ((x1,x2) --> (i1,i2)) = doms F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

set f = F9 /. x1;

set g = F9 /. x2;

A4: x1 in {x1,x2} by TARSKI:def 2;

then (doms ((x1,x2) --> (i1,i2))) /. x1 = dom (((x1,x2) --> (i1,i2)) /. x1) by Def1;

then dom (F9 /. x1) = dom (((x1,x2) --> (i1,i2)) /. x1) by A3, A4, Def1;

then A5: dom (F9 /. x1) = dom i1 by A1, Th3;

A6: x2 in {x1,x2} by TARSKI:def 2;

then (doms ((x1,x2) --> (i1,i2))) /. x2 = dom (((x1,x2) --> (i1,i2)) /. x2) by Def1;

then dom (F9 /. x2) = dom (((x1,x2) --> (i1,i2)) /. x2) by A3, A6, Def1;

then A7: dom (F9 /. x2) = dom i2 by A1, Th3;

cod (F9 /. x2) = b by A6, Th62;

then A8: F9 /. x2 in Hom ((dom i2),b) by A7;

cod (F9 /. x1) = b by A4, Th62;

then F9 /. x1 in Hom ((dom i1),b) by A5;

then consider h being Morphism of C such that

A9: h in Hom (c,b) and

A10: for k being Morphism of C st k in Hom (c,b) holds

( ( k (*) i1 = F9 /. x1 & k (*) i2 = F9 /. x2 ) iff h = k ) by A2, A8;

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

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

thus h in Hom (c,b) by A9; :: thesis: for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k )

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

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) )

assume A11: k in Hom (c,b) ; :: thesis: ( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k )

thus ( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

then A14: ( k (*) i1 = F9 /. x1 & k (*) i2 = F9 /. x2 ) by A10, A11;

let x be set ; :: thesis: ( x in {x1,x2} implies k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )

assume x in {x1,x2} ; :: thesis: k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

then ( x = x1 or x = x2 ) by TARSKI:def 2;

hence k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x by A1, A14, Th3; :: thesis: verum

end;then ( cod i1 = c & cod i2 = c ) ;

hence (x1,x2) --> (i1,i2) is Injections_family of c,{x1,x2} by Th65; :: according to CAT_3:def 17 :: thesis: for d being Object of C

for F9 being Injections_family of d,{x1,x2} st doms ((x1,x2) --> (i1,i2)) = doms F9 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

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Injections_family of b,{x1,x2} st doms ((x1,x2) --> (i1,i2)) = doms F9 holds

ex h being Morphism of C st

( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

let F9 be Injections_family of b,{x1,x2}; :: thesis: ( doms ((x1,x2) --> (i1,i2)) = doms F9 implies ex h being Morphism of C st

( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) ) )

assume A3: doms ((x1,x2) --> (i1,i2)) = doms F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

set f = F9 /. x1;

set g = F9 /. x2;

A4: x1 in {x1,x2} by TARSKI:def 2;

then (doms ((x1,x2) --> (i1,i2))) /. x1 = dom (((x1,x2) --> (i1,i2)) /. x1) by Def1;

then dom (F9 /. x1) = dom (((x1,x2) --> (i1,i2)) /. x1) by A3, A4, Def1;

then A5: dom (F9 /. x1) = dom i1 by A1, Th3;

A6: x2 in {x1,x2} by TARSKI:def 2;

then (doms ((x1,x2) --> (i1,i2))) /. x2 = dom (((x1,x2) --> (i1,i2)) /. x2) by Def1;

then dom (F9 /. x2) = dom (((x1,x2) --> (i1,i2)) /. x2) by A3, A6, Def1;

then A7: dom (F9 /. x2) = dom i2 by A1, Th3;

cod (F9 /. x2) = b by A6, Th62;

then A8: F9 /. x2 in Hom ((dom i2),b) by A7;

cod (F9 /. x1) = b by A4, Th62;

then F9 /. x1 in Hom ((dom i1),b) by A5;

then consider h being Morphism of C such that

A9: h in Hom (c,b) and

A10: for k being Morphism of C st k in Hom (c,b) holds

( ( k (*) i1 = F9 /. x1 & k (*) i2 = F9 /. x2 ) iff h = k ) by A2, A8;

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

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )

thus h in Hom (c,b) by A9; :: thesis: for k being Morphism of C st k in Hom (c,b) holds

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k )

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

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) )

assume A11: k in Hom (c,b) ; :: thesis: ( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k )

thus ( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )

proof

assume
h = k
; :: thesis: for x being set st x in {x1,x2} holds
assume A12:
for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ; :: thesis: h = k

then k (*) (((x1,x2) --> (i1,i2)) /. x2) = F9 /. x2 by A6;

then A13: k (*) i2 = F9 /. x2 by A1, Th3;

k (*) (((x1,x2) --> (i1,i2)) /. x1) = F9 /. x1 by A4, A12;

then k (*) i1 = F9 /. x1 by A1, Th3;

hence h = k by A10, A11, A13; :: thesis: verum

end;k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ; :: thesis: h = k

then k (*) (((x1,x2) --> (i1,i2)) /. x2) = F9 /. x2 by A6;

then A13: k (*) i2 = F9 /. x2 by A1, Th3;

k (*) (((x1,x2) --> (i1,i2)) /. x1) = F9 /. x1 by A4, A12;

then k (*) i1 = F9 /. x1 by A1, Th3;

hence h = k by A10, A11, A13; :: thesis: verum

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

then A14: ( k (*) i1 = F9 /. x1 & k (*) i2 = F9 /. x2 ) by A10, A11;

let x be set ; :: thesis: ( x in {x1,x2} implies k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )

assume x in {x1,x2} ; :: thesis: k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

then ( x = x1 or x = x2 ) by TARSKI:def 2;

hence k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x by A1, A14, Th3; :: thesis: verum

then A16: (x1,x2) --> (i1,i2) is Injections_family of c,{x1,x2} ;

x2 in {x1,x2} by TARSKI:def 2;

then A17: cod (((x1,x2) --> (i1,i2)) /. x2) = c by A16, Th62;

x1 in {x1,x2} by TARSKI:def 2;

then cod (((x1,x2) --> (i1,i2)) /. x1) = c by A16, Th62;

hence ( cod i1 = c & cod i2 = c ) by A1, A17, Th3; :: 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

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

A19: 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 ) ) )

( cod f = d & cod g = d ) by A18, A19, CAT_1:1;

then reconsider F9 = (x1,x2) --> (f,g) as Injections_family of d,{x1,x2} by Th65;

doms ((x1,x2) --> (i1,i2)) = (x1,x2) --> ((dom i1),(dom i2)) by Th6

.= (x1,x2) --> ((dom f),(dom i2)) by A18, CAT_1:1

.= (x1,x2) --> ((dom f),(dom g)) by A19, CAT_1:1

.= doms F9 by Th6 ;

then consider h being Morphism of C such that

A20: h in Hom (c,d) and

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

( ( for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) by A15;

take h ; :: thesis: ( 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 ) ) )

thus h in Hom (c,d) by A20; :: thesis: for k being Morphism of C st k in Hom (c,d) holds

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

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

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

thus ( k (*) i1 = f & k (*) i2 = g implies h = k ) :: thesis: ( h = k implies ( k (*) i1 = f & k (*) i2 = g ) )

proof

assume A24:
h = k
; :: thesis: ( k (*) i1 = f & k (*) i2 = g )
assume A23:
( k (*) i1 = f & k (*) i2 = g )
; :: thesis: h = k

end;now :: thesis: for x being set st x in {x1,x2} holds

k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

hence
h = k
by A21, A22; :: thesis: verumk (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

let x be set ; :: thesis: ( x in {x1,x2} implies k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )

assume x in {x1,x2} ; :: thesis: k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

then ( x = x1 or x = x2 ) by TARSKI:def 2;

then ( ( ((x1,x2) --> (i1,i2)) /. x = i1 & F9 /. x = f ) or ( ((x1,x2) --> (i1,i2)) /. x = i2 & F9 /. x = g ) ) by A1, Th3;

hence k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x by A23; :: thesis: verum

end;assume x in {x1,x2} ; :: thesis: k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x

then ( x = x1 or x = x2 ) by TARSKI:def 2;

then ( ( ((x1,x2) --> (i1,i2)) /. x = i1 & F9 /. x = f ) or ( ((x1,x2) --> (i1,i2)) /. x = i2 & F9 /. x = g ) ) by A1, Th3;

hence k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x by A23; :: thesis: verum

x2 in {x1,x2} by TARSKI:def 2;

then k (*) (((x1,x2) --> (i1,i2)) /. x2) = F9 /. x2 by A21, A22, A24;

then A25: k (*) (((x1,x2) --> (i1,i2)) /. x2) = g by A1, Th3;

x1 in {x1,x2} by TARSKI:def 2;

then k (*) (((x1,x2) --> (i1,i2)) /. x1) = F9 /. x1 by A21, A22, A24;

then k (*) (((x1,x2) --> (i1,i2)) /. x1) = f by A1, Th3;

hence ( k (*) i1 = f & k (*) i2 = g ) by A1, A25, Th3; :: thesis: verum