theorem :: INDEX_1:9

for C being Category
for I being Indexing of C
for c1, c2 being Object of C st not Hom (c1,c2) is empty holds
for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c1,(I `1) . c2