let C, D be Category; :: thesis: for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I holds rng (I * F) is Subcategory of T
let F be Functor of C,D; :: thesis: for I being Indexing of D
for T being TargetCat of I holds rng (I * F) is Subcategory of T
let I be Indexing of D; :: thesis: for T being TargetCat of I holds rng (I * F) is Subcategory of T
let T be TargetCat of I; :: thesis: rng (I * F) is Subcategory of T
T is TargetCat of I * F by Th24;
hence rng (I * F) is Subcategory of T by Th14; :: thesis: verum