:: deftheorem Def17 defines is_product_of CAT_8:def 17 :
for C1, C2, D being category
for P1 being Functor of D,C1 st P1 is covariant holds
for P2 being Functor of D,C2 st P2 is covariant holds
( D,P1,P2 is_product_of C1,C2 iff for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant holds
ex H being Functor of D1,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) ) );