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;
INDEX_1:def 9 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;
[[((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
;
verum
end;
then reconsider T = T as strict TargetCat of I ;
take
T
; for T being TargetCat of I holds T = Image (I -functor (C,T))
let T9 be TargetCat of I; T = Image (I -functor (C,T9))
thus
T = Image (I -functor (C,T9))
by Th11, CAT_5:22; verum