A4: Hom b,(a + b) <> {} by Th66;
( a + b is_a_coproduct_wrt in1 a,b, in2 a,b & Hom a,(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, A4, CAT_3:87;
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
A6: ( h1 * (in1 a,b) = f & h1 * (in2 a,b) = g ) and
A7: ( h2 * (in1 a,b) = f & h2 * (in2 a,b) = g ) ; :: thesis: h1 = h2
h1 = h by A6, A5;
hence h1 = h2 by A7, A5; :: thesis: verum