let C be Cocartesian_category; :: thesis: for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds
( in1 (a,b) is coretraction & in2 (a,b) is coretraction )
let a, b be Object of C; :: thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) )
A1: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th61;
( a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) & dom (in1 (a,b)) = a ) by Def26;
hence ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) ) by A1, CAT_3:82; :: thesis: verum