let C be Cocartesian_category; :: thesis: for a, b, c being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
Hom ((a + b),c) <> {}
let a, b, c 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 Def26;
( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th61;
hence ( Hom (a,c) <> {} & Hom (b,c) <> {} implies Hom ((a + b),c) <> {} ) by A1, CAT_3:81; :: thesis: verum