for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I
for J being Indexing of T holds (J * I) * F = J * (I * F)