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