for C being with_binary_products category
for a, b, c, d being Object of C st Hom (a,b) <> {} & Hom (c,d) <> {} holds
Hom ((a [x] c),(b [x] d)) <> {}