:: deftheorem defines -indexing_of INDEX_1:def 15 :
for C being Category
for D being Categorial Category
for F being Functor of C,D holds F -indexing_of C = [(Obj F),(pr2 F)];