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 I * F = ((I -functor D,T) * F) -indexing_of C
let F be Functor of C,D; :: thesis: for I being Indexing of D
for T being TargetCat of I holds I * F = ((I -functor D,T) * F) -indexing_of C
let I be Indexing of D; :: thesis: for T being TargetCat of I holds I * F = ((I -functor D,T) * F) -indexing_of C
let T be TargetCat of I; :: thesis: I * F = ((I -functor D,T) * F) -indexing_of C
( Image F is Subcategory of D & I -functor D,(rng I) = I -functor D,T ) by Th11;
then ( (I -functor D,(rng I)) * F = (I -functor D,T) * F & I * F = ((I -functor D,(rng I)) * F) -indexing_of C ) by Def16;
hence I * F = ((I -functor D,T) * F) -indexing_of C by Th2; :: thesis: verum