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
for J being Indexing of T holds (J * I) * F = J * (I * F)
let F be Functor of C,D; :: thesis: for I being Indexing of D
for T being TargetCat of I
for J being Indexing of T holds (J * I) * F = J * (I * F)
let I be Indexing of D; :: thesis: for T being TargetCat of I
for J being Indexing of T holds (J * I) * F = J * (I * F)
let T be TargetCat of I; :: thesis: for J being Indexing of T holds (J * I) * F = J * (I * F)
let J be Indexing of T; :: thesis: (J * I) * F = J * (I * F)
A1: ( I * F = ((I -functor (D,T)) * F) -indexing_of C & Image ((I -functor (D,T)) * F) is Subcategory of T ) by Th23;
T is TargetCat of I * F by Th24;
then rng (I * F) is Subcategory of T by Th14;
then A2: Image ((I * F) -functor (C,(rng (I * F)))) is Subcategory of T by CAT_5:4;
thus (J * I) * F = (J * (I -functor (D,T))) * F by Th32
.= J * ((I -functor (D,T)) * F) by Th26
.= J * (I * F) by A1, A2, Th18, Th22 ; :: thesis: verum