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

proof

the carrier of T = rng (Obj (I -functor C,S)) by CAT_5:def 3;
then A3: the carrier of T = rng (I `1 ) by Lm2;
dom (I `1 ) = the carrier of C by PARTFUN1:def 4;
hence for a being Object of C holds (I `1 ) . a is Object of T by A3, FUNCT_1:def 5; :: 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