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