theorem Th20: :: INDEX_1:20

for C being Category
for I being Indexing of C
for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2