let C be Cocartesian_category; :: thesis: for a, b being Object of C holds (id a) + (id b) = id (a + b)
let a, b be Object of C; :: thesis: (id a) + (id b) = id (a + b)
Hom (b,(a + b)) <> {} by Th61;
then A1: (in2 (a,b)) * (id b) = in2 (a,b) by CAT_1:29;
Hom (a,(a + b)) <> {} by Th61;
then (in1 (a,b)) * (id a) = in1 (a,b) by CAT_1:29;
hence (id a) + (id b) = id (a + b) by A1, Th66; :: thesis: verum