theorem :: INDEX_1:12

for C being Category
for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1 by Lm3;