A2: a + b is_a_coproduct_wrt in1 a,b, in2 a,b by Def27;
( Hom a,(a + b) <> {} & Hom b,(a + b) <> {} ) by Th66;
then consider h being Morphism of a + b,c such that
A3: for k being Morphism of a + b,c holds
( ( k * (in1 a,b) = f & k * (in2 a,b) = g ) iff h = k ) by A1, A2, CAT_3:87;
take h ; :: thesis: ( h * (in1 a,b) = f & h * (in2 a,b) = g )
thus ( h * (in1 a,b) = f & h * (in2 a,b) = g ) by A3; :: thesis: verum