let C be Cocartesian_category; :: thesis: for a, c, b being Object of C st Hom a,c <> {} & Hom b,c <> {} holds
Hom (a + b),c <> {}
let a, c, b be Object of C; :: thesis: ( Hom a,c <> {} & Hom b,c <> {} implies Hom (a + b),c <> {} )
( Hom a,(a + b) <> {} & Hom b,(a + b) <> {} & a + b is_a_coproduct_wrt in1 a,b, in2 a,b ) by Def27, Th66;
hence ( Hom a,c <> {} & Hom b,c <> {} implies Hom (a + b),c <> {} ) by CAT_3:87; :: thesis: verum