:: deftheorem Def3 defines Image CAT_5:def 3 :
for C, D being Category
for F being Functor of C,D
for b₄ being strict Subcategory of D holds
( b₄ = Image F iff ( the carrier of b₄ = rng (Obj F) & rng F c= the carrier' of b₄ & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
b₄ is Subcategory of E ) ) );