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