for C being Category
for D, E being Categorial Category
for F being Functor of C,D
for G being Functor of C,E st F = G holds
F -indexing_of C = G -indexing_of C by Th2;