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 )

proof

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 ) by Def19;
hence x1,x2 --> i1,i2 is Injections_family of c,{x1,x2} by Th70; :: according to CAT_3:def 18 :: 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 Def3;
then dom (F9 /. x1) = dom ((x1,x2 --> i1,i2) /. x1) by A3, A4, Def3;
then A5: dom (F9 /. x1) = dom i1 by A1, Th7;
A6: x2 in {x1,x2} by TARSKI:def 2;
then (doms (x1,x2 --> i1,i2)) /. x2 = dom ((x1,x2 --> i1,i2) /. x2) by Def3;
then dom (F9 /. x2) = dom ((x1,x2 --> i1,i2) /. x2) by A3, A6, Def3;
then A7: dom (F9 /. x2) = dom i2 by A1, Th7;
cod (F9 /. x2) = b by A6, Th67;
then A8: F9 /. x2 in Hom (dom i2),b by A7;
cod (F9 /. x1) = b by A4, Th67;
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, Def19;
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 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, Th7;
k * ((x1,x2 --> i1,i2) /. x1) = F9 /. x1 by A4, A12;
then k * i1 = F9 /. x1 by A1, Th7;
hence h = k by A10, A11, A13; :: thesis: verum

end;

assume h = k ; :: thesis: for x being set st x in {x1,x2} holds
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, Th7; :: thesis: verum

end;

assume A15: c is_a_coproduct_wrt x1,x2 --> i1,i2 ; :: thesis: c is_a_coproduct_wrt i1,i2
then A16: x1,x2 --> i1,i2 is Injections_family of c,{x1,x2} by Def18;
x2 in {x1,x2} by TARSKI:def 2;
then A17: cod ((x1,x2 --> i1,i2) /. x2) = c by A16, Th67;
x1 in {x1,x2} by TARSKI:def 2;
then cod ((x1,x2 --> i1,i2) /. x1) = c by A16, Th67;
hence ( cod i1 = c & cod i2 = c ) by A1, A17, Th7; :: according to CAT_3:def 19 :: 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:18;
then reconsider F9 = x1,x2 --> f,g as Injections_family of d,{x1,x2} by Th70;
doms (x1,x2 --> i1,i2) = x1,x2 --> (dom i1),(dom i2) by Th10
.= x1,x2 --> (dom f),(dom i2) by A18, CAT_1:18
.= x1,x2 --> (dom f),(dom g) by A19, CAT_1:18
.= doms F9 by Th10 ;
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, Def18;
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 A23: ( k * i1 = f & k * i2 = g ) ; :: thesis: h = k

now

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, Th7;
hence k * ((x1,x2 --> i1,i2) /. x) = F9 /. x by A23; :: thesis: verum

end;

hence h = k by A21, A22; :: thesis: verum

end;

assume A24: h = k ; :: thesis: ( 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, Th7;
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, Th7;
hence ( k * i1 = f & k * i2 = g ) by A1, A25, Th7; :: thesis: verum