:: deftheorem Def18 defines categorical_product CAT_8:def 18 :
for C1, C2 being category
for b₃ being triple object holds
( b₃ is categorical_product of C1,C2 iff ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( b₃ = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 ) );