:: deftheorem Def12 defines categorical_product CAT_8:def 12 :
for C being with_binary_products category
for c1, c2 being Object of C
for b₄ being triple object holds
( b₄ is categorical_product of c1,c2 iff ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st
( b₄ = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 ) );