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