let C be Category; :: thesis: for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & Hom (dom i1),(dom i2) <> {} & Hom (dom i2),(dom i1) <> {} holds
( i1 is coretraction & i2 is coretraction )
let c be Object of C; :: thesis: for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & Hom (dom i1),(dom i2) <> {} & Hom (dom i2),(dom i1) <> {} holds
( i1 is coretraction & i2 is coretraction )
let i1, i2 be Morphism of C; :: thesis: ( c is_a_coproduct_wrt i1,i2 & Hom (dom i1),(dom i2) <> {} & Hom (dom i2),(dom i1) <> {} implies ( i1 is coretraction & i2 is coretraction ) )
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: ( Hom (dom i1),(dom i2) <> {} & Hom (dom i2),(dom i1) <> {} ) ; :: thesis: ( i1 is coretraction & i2 is coretraction )
set I = {0 ,1};
set F = 0 ,1 --> i1,i2;
A3: ( (0 ,1 --> i1,i2) /. 0 = i1 & (0 ,1 --> i1,i2) /. 1 = i2 ) by Th7;

now

( cod i1 = c & cod i2 = c ) by A1, Def19;
hence 0 ,1 --> i1,i2 is Injections_family of c,{0 ,1} by Th70; :: thesis: ( c is_a_coproduct_wrt 0 ,1 --> i1,i2 & ( for x1, x2 being set st x1 in {0 ,1} & x2 in {0 ,1} holds
Hom (dom ((0 ,1 --> i1,i2) /. x1)),(dom ((0 ,1 --> i1,i2) /. x2)) <> {} ) )
thus c is_a_coproduct_wrt 0 ,1 --> i1,i2 by A1, Th85; :: thesis: for x1, x2 being set st x1 in {0 ,1} & x2 in {0 ,1} holds
Hom (dom ((0 ,1 --> i1,i2) /. x1)),(dom ((0 ,1 --> i1,i2) /. x2)) <> {}
let x1, x2 be set ; :: thesis: ( x1 in {0 ,1} & x2 in {0 ,1} implies Hom (dom ((0 ,1 --> i1,i2) /. x1)),(dom ((0 ,1 --> i1,i2) /. x2)) <> {} )
assume ( x1 in {0 ,1} & x2 in {0 ,1} ) ; :: thesis: Hom (dom ((0 ,1 --> i1,i2) /. x1)),(dom ((0 ,1 --> i1,i2) /. x2)) <> {}
then ( ( x1 = 0 or x1 = 1 ) & ( x2 = 0 or x2 = 1 ) ) by TARSKI:def 2;
hence Hom (dom ((0 ,1 --> i1,i2) /. x1)),(dom ((0 ,1 --> i1,i2) /. x2)) <> {} by A2, A3, CAT_1:56; :: thesis: verum

end;

then ( 0 in {0 ,1} & 1 in {0 ,1} & ( for x being set st x in {0 ,1} holds
(0 ,1 --> i1,i2) /. x is coretraction ) ) by Th79, TARSKI:def 2;
hence ( i1 is coretraction & i2 is coretraction ) by A3; :: thesis: verum