A4: a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) by Def8;
( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19;
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, A4, CAT_3:55;
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
A6: ( (pr1 (a,b)) * h1 = f & (pr2 (a,b)) * h1 = g ) and
A7: ( (pr1 (a,b)) * h2 = f & (pr2 (a,b)) * h2 = g ) ; :: thesis: h1 = h2
h1 = h by A6, A5;
hence h1 = h2 by A7, A5; :: thesis: verum