:: deftheorem Def10 defines Indexing INDEX_1:def 10 :
for A, B being non empty set
for F, G being Function of B,A
for c being PartFunc of [:B,B:],B
for i being Function of A,B st ex C being Category st C = CatStr(# A,B,F,G,c #) holds
for b₇ being Indexing of F,G holds
( b₇ is Indexing of F,G,c,i iff ( ( for a being Element of A holds (b₇ `2) . (i . a) = id ((b<sub>7</sub> `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b₇ `2) . (c . [m2,m1]) = ((b<sub>7</sub> `2) . m2) * ((b₇ `2) . m1) ) ) );