theorem Th23: :: INDEX_1:23

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 I * F = ((I -functor (D,T)) * F) -indexing_of C