theorem :: INDEX_1:13

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