:: deftheorem defines * INDEX_1:def 18 :
for C, D being Category
for I1 being Indexing of C
for I2 being Indexing of D holds I2 * I1 = I2 * (I1 -functor (C,(rng I1)));