:: deftheorem Def17 defines * INDEX_1:def 17 :
for C being Category
for I being Indexing of C
for D being Categorial Category st D is TargetCat of I holds
for E being Categorial Category
for F being Functor of D,E
for b₆ being Indexing of C holds
( b₆ = F * I iff for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b₆ = (G * (I -functor (C,T))) -indexing_of C );