:: deftheorem Def12 defines rng INDEX_1:def 12 :
for C being Category
for I being Indexing of C
for b₃ being strict TargetCat of I holds
( b₃ = rng I iff for T being TargetCat of I holds b₃ = Image (I -functor (C,T)) );