:: deftheorem Def22 defines [x] CAT_8:def 22 :
for C1, C2, D1, D2 being category
for F1 being Functor of C1,D1
for F2 being Functor of C2,D2 st F1 is covariant & F2 is covariant holds
for b₇ being Functor of (C1 [x] C2),(D1 [x] D2) holds
( b₇ = F1 [x] F2 iff ( b₇ is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b₇ & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b₇ ) );