let C be Cocartesian_category; :: thesis: for a, b, c, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a + b),(c + d)) <> {}
let a, b, c, d be Object of C; :: thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} implies Hom ((a + b),(c + d)) <> {} )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,d) <> {} ; :: thesis: Hom ((a + b),(c + d)) <> {}
Hom (d,(c + d)) <> {} by Th61;
then A3: Hom (b,(c + d)) <> {} by A2, CAT_1:24;
Hom (c,(c + d)) <> {} by Th61;
then Hom (a,(c + d)) <> {} by A1, CAT_1:24;
hence Hom ((a + b),(c + d)) <> {} by A3, Th65; :: thesis: verum