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