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 T is TargetCat of I * F
let F be Functor of C,D; :: thesis: for I being Indexing of D
for T being TargetCat of I holds T is TargetCat of I * F
let I be Indexing of D; :: thesis: for T being TargetCat of I holds T is TargetCat of I * F
let T be TargetCat of I; :: thesis: T is TargetCat of I * F
set T9 = the TargetCat of I * F;
( rng (I * F) = Image ((I * F) -functor (C, the TargetCat of I * F)) & I * F = ((I -functor (D,T)) * F) -indexing_of C ) by Def12, Th23;
then rng (I * F) = Image ((I -functor (D,T)) * F) by Th18, CAT_5:22;
hence T is TargetCat of I * F by Th14; :: thesis: verum