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 Th61;
then A2: (id (a + b)) * (in2 (a,b)) = in2 (a,b) by CAT_1:28;
A3: Hom (a,(a + b)) <> {} by Th61;
then (id (a + b)) * (in1 (a,b)) = in1 (a,b) by CAT_1:28;
hence [$(in1 (a,b)),(in2 (a,b))$] = id (a + b) by A3, A1, A2, Def28; :: thesis: verum