let C be Category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for F being Functor of T,D holds Image F is TargetCat of F * I
let F be Functor of T,D; :: thesis: Image F is TargetCat of F * I
reconsider F' = F as Functor of T, Image F by CAT_5:8;
consider T' being TargetCat of F * I;
A1: rng (F * I) = Image ((F * I) -functor C,T') by Def12;
F * I = F' * I by Th27
.= (F' * (I -functor C,T)) -indexing_of C by Def17 ;
then rng (F * I) = Image (F' * (I -functor C,T)) by A1, Th18, CAT_5:22;
hence Image F is TargetCat of F * I by Th14; :: thesis: verum