theorem Th42: :: CAT_8:42

for C being with_binary_products category
for a, b being Object of C holds
( a [x] b, pr1 (a,b), pr2 (a,b) is_product_of a,b & Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )