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 Def27;
then ( 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 Def27, CAT_3:def 19;
hence ( Hom a,(a + b) <> {} & Hom b,(a + b) <> {} ) by CAT_1:18; :: thesis: verum