for C being Category
for D being Categorial Category
for I1 being Indexing of C
for I2 being Indexing of D
for T being TargetCat of I1 st D is TargetCat of I1 holds
I2 * I1 = I2 * (I1 -functor (C,T))