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 D 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 D 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 D is TargetCat of F * I
let D be Categorial Category; :: thesis: for F being Functor of T,D holds D is TargetCat of F * I
let F be Functor of T,D; :: thesis: D is TargetCat of F * I
Image F is TargetCat of F * I by Th28;
then rng (F * I) is Subcategory of Image F by Th14;
then rng (F * I) is Subcategory of D by CAT_5:4;
hence D is TargetCat of F * I by Th14; :: thesis: verum