let C be Category; for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D holds Image F is TargetCat of F * I
let I be Indexing of C; for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D holds Image F is TargetCat of F * I
let T be TargetCat of I; for D being Categorial Category
for F being Functor of T,D holds Image F is TargetCat of F * I
let D be Categorial Category; for F being Functor of T,D holds Image F is TargetCat of F * I
let F be Functor of T,D; Image F is TargetCat of F * I
reconsider F9 = F as Functor of T, Image F by CAT_5:8;
set T9 = the TargetCat of F * I;
A1:
rng (F * I) = Image ((F * I) -functor (C, the TargetCat of F * I))
by Def12;
F * I =
F9 * I
by Th27
.=
(F9 * (I -functor (C,T))) -indexing_of C
by Def17
;
then
rng (F * I) = Image (F9 * (I -functor (C,T)))
by A1, Th18, CAT_5:22;
hence
Image F is TargetCat of F * I
by Th14; verum