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 ) )
( a + b is_a_coproduct_wrt in1 a,b, in2 a,b & dom (in1 a,b) = a & dom (in2 a,b) = b ) by Def27;
hence ( Hom a,b <> {} & Hom b,a <> {} implies ( in1 a,b is coretraction & in2 a,b is coretraction ) ) by CAT_3:88; :: thesis: verum