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 <> {} )
A1: a + b is_a_coproduct_wrt in1 a,b, in2 a,b by Def27;
( Hom a,(a + b) <> {} & Hom b,(a + b) <> {} ) by Th66;
hence ( Hom a,c <> {} & Hom b,c <> {} implies Hom (a + b),c <> {} ) by A1, CAT_3:87; :: thesis: verum