let C be Category; :: thesis: for a, c, b being Object of C
for i1 being Morphism of a,c
for i2 being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( i1 is coretraction & i2 is coretraction )
let a, c, b be Object of C; :: thesis: for i1 being Morphism of a,c
for i2 being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( i1 is coretraction & i2 is coretraction )
let i1 be Morphism of a,c; :: thesis: for i2 being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( i1 is coretraction & i2 is coretraction )
let i2 be Morphism of b,c; :: thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} implies ( i1 is coretraction & i2 is coretraction ) )
assume A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) ; :: thesis: ( not c is_a_coproduct_wrt i1,i2 or not Hom (a,b) <> {} or not Hom (b,a) <> {} or ( i1 is coretraction & i2 is coretraction ) )
assume that
A2: c is_a_coproduct_wrt i1,i2 and
A3: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: thesis: ( i1 is coretraction & i2 is coretraction )
set I = {0,1};
( cod i1 = c & cod i2 = c ) by A2, Def18;
then reconsider F = (0,1) --> (i1,i2) as Injections_family of c,{0,1} by Th65;
A4: F /. 0 = i1 by Th3;
A5: F /. 1 = i2 by Th3;

A6: now :: thesis: ( F is Injections_family of c,{0,1} & c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in {0,1} & x2 in {0,1} holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) )

thus F is Injections_family of c,{0,1} ; :: thesis: ( c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in {0,1} & x2 in {0,1} holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) )
thus c is_a_coproduct_wrt F by A2, Th79; :: thesis: for x1, x2 being set st x1 in {0,1} & x2 in {0,1} holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {}
let x1, x2 be set ; :: thesis: ( x1 in {0,1} & x2 in {0,1} implies Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} )
assume that
A7: x1 in {0,1} and
A8: x2 in {0,1} ; :: thesis: Hom ((dom (F /. x1)),(dom (F /. x2))) <> {}
A9: ( x2 = 0 or x2 = 1 ) by A8, TARSKI:def 2;
( x1 = 0 or x1 = 1 ) by A7, TARSKI:def 2;
then A10: ( dom (F /. x1) = a or dom (F /. x1) = b ) by A4, A5, A1, CAT_1:5;
( dom (F /. x2) = a or dom (F /. x2) = b ) by A9, A4, A5, A1, CAT_1:5;
hence Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} by A3, A10; :: thesis: verum

end;

A11: 1 in {0,1} by TARSKI:def 2;
A12: 0 in {0,1} by TARSKI:def 2;
( dom (F /. 0) = a & dom (F /. 1) = b ) by A4, A5, A1, CAT_1:5;
hence ( i1 is coretraction & i2 is coretraction ) by A4, A6, A11, Th73, A5, A12, A1; :: thesis: verum