:: deftheorem Def10 defines is_product_of CAT_8:def 10 :
for C being category
for a, b, c being Object of C
for p1 being Morphism of c,a st Hom (c,a) <> {} holds
for p2 being Morphism of c,b st Hom (c,b) <> {} holds
( c,p1,p2 is_product_of a,b iff for c1 being Object of C
for q1 being Morphism of c1,a
for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds
( Hom (c1,c) <> {} & ex h being Morphism of c1,c st
( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds
h = h1 ) ) ) );