theorem Th24: :: INDEX_1:24

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I holds T is TargetCat of I * F