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