theorem :: INDEX_1:17

for C being Category
for D being Categorial Category
for F being Functor of C,D holds D is TargetCat of F -indexing_of C