let C be Cocartesian_category; :: thesis: for a, b being Object of C holds
( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} )
let a, b be Object of C; :: thesis: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} )
set c = the Coproduct of C . (a,b);
set i1 = the Incl1 of C . (a,b);
set i2 = the Incl2 of C . (a,b);
the Coproduct of C . (a,b) is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26;
then A1: ( cod ( the Incl1 of C . (a,b)) = the Coproduct of C . (a,b) & cod ( the Incl2 of C . (a,b)) = the Coproduct of C . (a,b) ) ;
( dom ( the Incl1 of C . (a,b)) = a & dom ( the Incl2 of C . (a,b)) = b ) by Def26;
hence ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by A1, CAT_1:1; :: thesis: verum