:: deftheorem Def16 defines [x] CAT_8:def 16 :
for C being with_binary_products category
for a, b, c, d being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
for g being Morphism of c,d st Hom (c,d) <> {} holds
for b₈ being Morphism of a [x] c,b [x] d holds
( b₈ = f [x] g iff ( f * (pr1 (a,c)) = (pr1 (b,d)) * b₈ & g * (pr2 (a,c)) = (pr2 (b,d)) * b₈ ) );