:: deftheorem Def8 defines Indexing INDEX_1:def 8 :
for A, B being non empty set
for F, G being Function of B,A
for b₅ being Category-yielding_on_first ManySortedSet of A,B holds
( b₅ is Indexing of F,G iff b₅ `2 is ManySortedFunctor of (b<sub>5</sub> `1) * F,(b₅ `1) * G );