let C be Cocartesian_category; :: thesis: for a, b being Object of C holds [$(in1 a,b),(in2 a,b)$] = id (a + b)
let a, b be Object of C; :: thesis: [$(in1 a,b),(in2 a,b)$] = id (a + b)
A1: Hom b,(a + b) <> {} by Th66;
then A2: (id (a + b)) * (in2 a,b) = in2 a,b by CAT_1:57;
A3: Hom a,(a + b) <> {} by Th66;
then (id (a + b)) * (in1 a,b) = in1 a,b by CAT_1:57;
hence [$(in1 a,b),(in2 a,b)$] = id (a + b) by A3, A1, A2, Def29; :: thesis: verum