let C be Cocartesian_category; :: thesis: for a, c, b, d being Object of C st Hom a,c <> {} & Hom b,d <> {} holds
Hom (a + b),(c + d) <> {}
let a, c, b, 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 Th66;
then A3: Hom b,(c + d) <> {} by A2, CAT_1:52;
Hom c,(c + d) <> {} by Th66;
then Hom a,(c + d) <> {} by A1, CAT_1:52;
hence Hom (a + b),(c + d) <> {} by A3, Th70; :: thesis: verum