for C being Category
for I being Indexing of C
for D being TargetCat of I
for J being Indexing of D
for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)