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 by Th7;

A4: 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 that
A5: x1 in {0,1} and
A6: x2 in {0,1} ; :: thesis: Hom ((dom (((0,1) --> (i1,i2)) /. x1)),(dom (((0,1) --> (i1,i2)) /. x2))) <> {}
A7: ( x2 = 0 or x2 = 1 ) by A6, TARSKI:def 2;
( x1 = 0 or x1 = 1 ) by A5, TARSKI:def 2;
hence Hom ((dom (((0,1) --> (i1,i2)) /. x1)),(dom (((0,1) --> (i1,i2)) /. x2))) <> {} by A2, A3, A7, Th7, CAT_1:27; :: thesis: verum

end;

A8: 1 in {0,1} by TARSKI:def 2;
( ((0,1) --> (i1,i2)) /. 1 = i2 & 0 in {0,1} ) by Th7, TARSKI:def 2;
hence ( i1 is coretraction & i2 is coretraction ) by A3, A4, A8, Th79; :: thesis: verum