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