( cod (in1 (a,b)) = a + b & dom (in1 (a,b)) = a ) by Th64;
hence in1 (a,b) is Morphism of a,a + b by CAT_1:22; :: thesis: verum