let h1, h2 be Morphism of c,a [x] b; :: thesis: ( (pr1 a,b) * h1 = f & (pr2 a,b) * h1 = g & (pr1 a,b) * h2 = f & (pr2 a,b) * h2 = g implies h1 = h2 )
assume that
A3: ( (pr1 a,b) * h1 = f & (pr2 a,b) * h1 = g ) and
A4: ( (pr1 a,b) * h2 = f & (pr2 a,b) * h2 = g ) ; :: thesis: h1 = h2
( Hom (a [x] b),a <> {} & Hom (a [x] b),b <> {} & a [x] b is_a_product_wrt pr1 a,b, pr2 a,b ) by Def9, Th21;
then consider h being Morphism of c,a [x] b such that
A5: for h1 being Morphism of c,a [x] b holds
( ( (pr1 a,b) * h1 = f & (pr2 a,b) * h1 = g ) iff h = h1 ) by A1, CAT_3:60;
( h1 = h & h2 = h ) by A3, A4, A5;
hence h1 = h2 ; :: thesis: verum