( 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:4; :: thesis: verum