:: deftheorem Def16 defines * INDEX_1:def 16 :
for C, D, E being Category
for F being Functor of C,D
for I being Indexing of E st Image F is Subcategory of E holds
for b₆ being Indexing of C holds
( b₆ = I * F iff for F9 being Functor of C,E st F9 = F holds
b₆ = ((I -functor (E,(rng I))) * F9) -indexing_of C );