let h1, h2 be Morphism of a + b,c; :: thesis: ( h1 * (in1 a,b) = f & h1 * (in2 a,b) = g & h2 * (in1 a,b) = f & h2 * (in2 a,b) = g implies h1 = h2 )
assume that
A3: ( h1 * (in1 a,b) = f & h1 * (in2 a,b) = g ) and
A4: ( h2 * (in1 a,b) = f & h2 * (in2 a,b) = g ) ; :: thesis: h1 = h2
( a + b is_a_coproduct_wrt in1 a,b, in2 a,b & Hom a,(a + b) <> {} & Hom b,(a + b) <> {} ) by Def27, Th66;
then consider h being Morphism of a + b,c such that
A5: for k being Morphism of a + b,c holds
( ( k * (in1 a,b) = f & k * (in2 a,b) = g ) iff h = k ) by A1, CAT_3:87;
( h1 = h & h2 = h ) by A3, A4, A5;
hence h1 = h2 ; :: thesis: verum