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 a,(a + b) <> {} & Hom b,(a + b) <> {} ) by Th66;
then ( (id (a + b)) * (in1 a,b) = in1 a,b & (id (a + b)) * (in2 a,b) = in2 a,b ) by CAT_1:57;
hence [$(in1 a,b),(in2 a,b)$] = id (a + b) by A1, Def29; :: thesis: verum