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