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:56; :: 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