( 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