theorem :: INDEX_1:5

for C being Category
for I being Indexing of the Source of C, the Target of C
for m being Morphism of C holds (I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m) by Th4;