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