theorem Th57: :: CAT_8:57

for C1, C2 being non empty category
for D1, D2 being category
for F1 being Functor of C1,D1
for F2 being Functor of C2,D2
for c1 being morphism of C1
for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds
(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]