set S = the TargetCat of I;
reconsider T = Image (I -functor (C, the TargetCat of I)) as strict Subcategory of the TargetCat of I ;
reconsider F = I -functor (C, the TargetCat of I) as Functor of C,T by CAT_5:8;
T is TargetCat of I

proof

the carrier of T = rng (Obj (I -functor (C, the TargetCat of I))) by CAT_5:def 3;
then A3: the carrier of T = rng (I `1) by Lm3;
dom (I `1) = the carrier of C by PARTFUN1:def 2;
hence for a being Object of C holds (I `1) . a is Object of T by A3, FUNCT_1:def 3; :: according to INDEX_1:def 9 :: thesis: for b being Element of the carrier' of C holds [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of T
let b be Morphism of C; :: thesis: [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of T
F . b = [[((I `1) . (dom b)),((I `1) . (cod b))],((I `2) . b)] by Def11;
hence [[((I `1) . ( the Source of C . b)),((I `1) . ( the Target of C . b))],((I `2) . b)] is Morphism of T ; :: thesis: verum

end;

then reconsider T = T as strict TargetCat of I ;
take T ; :: thesis: for T being TargetCat of I holds T = Image (I -functor (C,T))
let T9 be TargetCat of I; :: thesis: T = Image (I -functor (C,T9))
thus T = Image (I -functor (C,T9)) by Th11, CAT_5:22; :: thesis: verum