theorem Th18: :: INDEX_1:18

for C being Category
for D being Categorial Category
for F being Functor of C,D
for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)